19-25 May 2018
Atherton CA, U.S.A.
Eighth Summer School on Formal Techniques, May 19 - May 25, 2018
Menlo College
Atherton, California
http://fm.csl.sri.com/SSFT18
Techniques based on formal logic, such as model checking,
satisfiability, static analysis, and automated theorem proving, are
finding a broad range of applications in modeling, analysis,
verification, and synthesis. This school, the sixth in the series, will
focus on the principles and practice of formal techniques, with a
strong emphasis on the hands-on use and development of this
technology. It primarily targets graduate students and young
researchers who are interested in studying and using formal techniques
in their research. A prior background in formal methods is helpful but
not required. Participants at the school can expect to have a seriously
fun time experimenting with the tools and techniques presented in the
lectures during laboratory sessions.
The lecturers at the school include:
* Emina Torlak (University of Washington)
Solver-Aided Programming
Abstract: Solver-aided tools have automated the verification and
synthesis of practical programs in many domains, from
high-performance computing to executable biology. These tools work
by reducing verification and synthesis tasks to satisfiability
queries, which involves compiling (bounded) programs to logical
constraints. The first lecture will cover the basics of symbolic
compilation for (bounded) program verification and synthesis. The
second lecture will cover an advanced, and rapid, way to construct
solver-aided tools by embedding them in Rosette, a solver-aided
programming language. Since its release in 2014, Rosette has enabled
a wide range of programmers, from professional developers to high
school students, to quickly create a variety of practical
solver-aided tools, from a verifier for radiation therapy software
to a synthesizer for algebra tutoring rules. The lab sessions will
use Rosette to demonstrate key ideas behind symbolic compilation and
solver-aided programming.
* Mooly Sagiv (Tel Aviv University)
Modularity for Decidability: Implementing and Semi-Automatically
Verifying Distributed Systems
Abstract: Proof automation can substantially increase productivity
in the formal verification of complex systems. However, the
unpredictablility of automated provers in handling quantified
formulas presents a major hurdle to usability of these tools. Here,
we propose to solve this problem not by improving the provers, but
by using a modular proof methodology that allows us to produce
decidable verification conditions. Decidability greatly improves the
predictability of proof automation, resulting in a more practical
verification approach. We apply this methodology to develop verified
implementations of distributed protocols with competitive
performance, showing its effectiveness.
This is a joint work with Marcelo Taube (TAU), Giuliano Losa(UCLA),
Ken McMillan (Microsoft Research), Oded Padon and Sharon
Shoham(TAU). The techniques have been implemented in IVY
https://www.microsoft.com/en-us/research/project/ivy/
* Nikhil Swamy and Jonathan Protzenko (Microsoft Research)
Programming and Proving in F* and Low*
Abstract: F* is an ML-like programming language aimed at program
verification. At its core is a type system based on dependent types,
refinement types and Hoare-style logics for user-defined monadic
effects. Together, these features allow expressing precise and
compact specifications for programs, including functional
correctness and security properties. The F* type-checker aims to
prove that programs meet their specifications using a combination of
SMT solving, user provided proof terms, as well as interactive
proofs using tactics.
This tutorial provides a general introduction to F* followed by a
focus on Low*, a subset of F* that extracts to C code for efficient,
low-level programming. The examples we present are drawn from
Project Everest, an ongoing effort using F* and Low* to verify and
deploy secure components in the HTTPS ecosystem, including protocols
such TLS and the cryptographic algorithms that underlie it.
* Andreas Abel (Chalmers/Gothenburg University)
Introduction to Dependent Types and Agda
Abstract: Dependent types integrate programming with rich types,
specifications, and verification into a single language. Dependent
types allow to express arbitrary logical properties of programs, and
correctness proofs can be woven into the code.
In this tutorial, I will give a brief introduction to dependent
types and the dependently-typed language Agda developed at Chalmers.
We will understand the theoretical concepts as we walk through some
representative use cases. In the first part, we will learn how to
elegantly represent binary search trees and their ordering invariant
in Agda. In the second part, we will look at examples from
programming language, like representation of expressions,
evaluation, and equational reasoning. The tutorial is accompanied
by Agda programming and reasoning exercises.
* Dirk Beyer (Ludwig Maximilian University, Munich, Germany)
Software Model Checking
The main lectures in the summer school will be preceded by a background
course on logic on
* Natarajan Shankar (SRI CSL) and Stephane Graham-Lengrand (Ecole
Polytechnique) Speaking Logic
Abstract: Formal logic has become the lingua franca of computing. It
is used for specifying digital systems, annotating programs with
assertions, defining the semantics of programming languages, and
proving or refuting claims about software or hardware
systems. Familiarity with the language and methods of logic is a
foundation for research into formal aspects of computing. This course
covers the basics of logic focusing on the use of logic as a medium
for formalization and proof.
We will also have invited talks by
* Nina Narodytska (VMWare Research)
Verifying Properties of Binarized Deep Neural Networks
* Gordon Plotkin (U. Edinburgh, UK)
Some Principles of Differentiable Programming Languages Research Papers
* Edward A. Lee (UC Berkeley)
Plato and the Nerd - The Creative Partnership of Humans and Technology
Information about previous Summer Schools on Formal Techniques can be
found at
http://fm.csl.sri.com/SSFT11
http://fm.csl.sri.com/SSFT12
http://fm.csl.sri.com/SSFT13
http://fm.csl.sri.com/SSFT14
http://fm.csl.sri.com/SSFT15
http://fm.csl.sri.com/SSFT16
http://fm.csl.sri.com/SSFT17
We expect to provide support for the travel and accommodation for (a
limited number of) students registered at US universities. We welcome
applications from non-US students as well as non-students (if space
permits). Non-US students will have to cover their own travel and will
be charged around US$800 for meals and lodging. Applications should be
submitted at the website http://fm.csl.sri.com/SSFT18
Applicants are urged to submit their applications before April 30,
2018, since there are only a limited number of spaces available.
Non-US applicants requiring US visas are requested to apply early. We
strongly encourage the participation of women and under-represented
minorities in the summer school.
--
[LOGIC] mailing list
http://www.dvmlg.de/mailingliste.html
Archive: http://www.illc.uva.nl/LogicList/
provided by a collaboration of the DVMLG, the Maths Departments in Bonn and Hamburg, and the ILLC at the Universiteit van Amsterdam