Fourth Summer School on Formal Techniques

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 fourth 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 developing and using formal techniques in their research. A prior background in formal methods is helpful but not required. Participants at the school will have a seriously fun time experimenting with the tools and techniques presented in the lectures during laboratory sessions.

The lecturers at the school include:

• Nikolaj Bjorner (MSR Redmond):
  Software verification with SMT (Slides1, Slides2, SMT Applications, samples.zip)
  Abstract: Satisfiability Modulo Theories (SMT) solvers offer a compelling match for static software analysis, since several common software constructs map directly into supported theories. The lecture takes as starting point the state-of-the art SMT solver Z3, developed at Microsoft Research and the use of it for software verification. In the first lecture we examine connections from program logics to SMT solving. We use the VeriCon tool as starting point for illustrating verification condition generation. VeriCon is a prototype tool for verification of Software Defined Network controller programs. In the second lecture we revisit a central problem in program analysis, model checking and verification - synthesizing sufficient inductive invariants. It is formulated as solving satisfiability of Horn clauses: We exploit that models of constrained Horn clauses correspond directly to certificates of program correctness. We examine algorithms used in software model checking as strategies for solving Horn clauses. These algorithms include, variants of bounded model checking, symbolic execution, bottom-up saturation with finite relations, such as hash tables, BDDs and three-valued bit-vectors, backwards chaining with tabling, fold-unfold transformations, variants inspired by IC3 and interpolation procedures. Z3 contains implementations of most of these algorithms and they are used in various program and network analysis applications. In the lab exercises we will rely on Z3’s Python bindings to complete encodings of various program analysis problems.
• Veronique Cortier (LORIA, France):
  Formal analysis of security protocols: Models, Techniques, and Tools
  Abstract: Security protocols aims at securing communications over untrusted networks such as Internet. Their design is notoriously error-prone, with flaws discovered years later. Formal methods have been successful in reasoning about the security of protocols and detect attacks. Automatic tools have been designed and applied to many protocols, from academic ones to deployed protocols such as SSL or Kerberos. In these lectures, we explain how security protocols can be modeled in symbolic models such as Horn clauses (a fragment of first-order logic) or applied-pi calculus (a process algebra). We describe and discuss decision techniques to automatically verify properties such as authentication or confidentiality.

  These lectures will also be the opportunity to play a "security game" where students design security protocols of their own and find flaws in other protocols using some existing automatic tools.

• Gerard Holzmann (JPL/Caltech):
  Verifying Safety Critical Code (Resources)
  Abstract: Formal software verification, for instance based on automata-theoretic verification and logic model checking, is not just interesting from a purely academic point of view, it has also become a necessity in the development of safety critical code. Failure of safety critical code can endanger lives, or have significant economic consequences. We'll discuss some new approaches to this decades old problem that target the verification of implementation level source code directly, using model extraction, and massively parallel search algorithms.
• Gerwin Klein (NICTA Australia):
  Programming language semantics in Isabelle (Exercises, Solutions, Reg.thy, Demos)
  Abstract: After a brief crash course on the interactive proof assistant Isabelle, this lecture will show how to formalise the semantics of a small imperative programming language in the theorem prover, and how to use Isabelle to reason about programs and programming languages. The lecture will cover the topics of big and small-step operational semantics, their equivalence, a small type system, and a type soundness proof. Further, deeper reaching teaching material is available.
• Marta Kwiatkowska (University of Oxford):
  Probabilistic model checking with PRISM (Resources)
  Abstract: Probabilistic model checking is a formal verication technique for the analysis of systems that exhibit stochastic behaviour. Such behaviour occurs, for example, due to component failure or randomisation, commonly used as a symmetry breaker in distributed coordination and communication protocols. The techniques have been implemented in PRISM (www.prismmodelchecker.org) and enable a range of quantitative analyses of probabilistic models against specifications such as the worst-case probability of failure within 10 seconds or the minimum expected power consumption over all possible schedulings. This tutorial will give an introduction to probabilistic model checking, explaining the underlying theory and algorithms for model checking and strategy synthesis. The material will be illustrated with several case studies that have been modelled and analysed in PRISM.
• Natarajan Shankar (SRI CSL):
  Speaking Logic (Slides)
  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.

Invited speakers at the school include:

• Dana Scott (CMU):
  Lambda Calculus: History, Models, Future (Handout, ACMTuring, JAL2014, Types)
• Emina Torlak (UC Berkeley):
  Programming for Everyone: From Solvers to Solver-Aided Languages and Beyond (Slides)

Student presentations include:

• Srinivas Neduri (Rice University):
  ROBOSYNTH: SMT-Based Synthesis of Integrated Task and Motion Plans from Plan Outlines (Slides)
• Vũ Lê (UC Davis):
  Compiler Validation via Equivalence Modulo Input (Slides)
• Nimit Singhania (U Penn):
  Piecewise Affine Models from Input-Output Data (Slides)
• Amer Tahat (Michigan Technological University):
  Mechanical Verification of Avicenna’s Proof on the Existence of a Necessary Existent and Its Unity (Slides, PVS Specification)
• Ulya Bayram (U Miami):
  Predictive Modeling (Slides )
• Paolo Masci (Queen Mary University of London):
  Formal Verification of medical user interface software in PVS (Slides )