[FOM] Eighth Summer School on Formal Techniques, Menlo College, Atherton California, May 19-25, 2018

[Natarajan Shankar]

  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.