Seventh 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 seventh 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.

Note: The school is preceded by the 9th NASA Formal Methods Symposium (NFM) 2017 and the associated sixth Automated Formal Methods (AFM) workshop. On May 20 there will be an AFM tutorial day that students are encouraged to attend.

Lecturers

Stephanie Delaune (IRISA France), Marijn Heule (University of Texas at Austin), K. Rustan M. Leino (Microsoft Research, Redmond WA), Sam Blackshear (Facebook), and Ashish Tiwari (SRI)

• Stephanie Delaune (IRISA France):
  Verification of security protocols: from confidentiality to privacy
  (ProVerif)
  Abstract: Security protocols are widely used today to secure transactions that take place through public channels like the Internet. Typical functionalities are the transfer of a credit card number or the authentication of a user on a system. Because of their increasing ubiquity in many important applications (e.g. electronic commerce, smartphone, government-issued ID . . . ), a very important research challenge consists in developing methods and verification tools to increase our trust on security protocols, and so on the applications that rely on them.

  Formal methods offer symbolic models to carefully analyse security protocols, together with a set of proof techniques and efficient tools such as ProVerif. These methods build on techniques from model-checking, automated reasoning and concurrency theory. We will explain how security protocols as well as the security properties they are supposed to achieve are formalised in symbolic models. Then, we will describe and discuss techniques to automatically verify different kinds of security properties. The lab sessions will be the opportunity to play with the ProVerif verification tool.

  Bio: Dr. Stephanie Delaune is a CNRS researcher at IRISA Rennes. She received her PhD in 2006 and presented her Habilitation thesis in 2011. She won a France Telecom award for her PhD thesis. Dr. Delaune has a made a number of significant contributions to the modeling and automated verification of cryptographic protocols.
• Marijn Heule (University of Texas at Austin):
  State-of-the-art SAT Solving
  ( Glucose 3.0 (not the later versions), Slides1, Slides2)
  Abstract: Satisfiability (SAT) solvers have become powerful search engines to solve a wide range of applications in fields such as formal verification, planning and bio-informatics. Due to the elementary representation of SAT problems, many low-level optimizations can be implemented. At the same time, there exist clause-based techniques that can simulate several high-level reasoning methods. The teaching session focuses on the search procedures in successful conflict-driven clause learning SAT solvers. It shows how to learn from conflicts and provides an overview of effective heuristics for variable and value selection. Additionally, the teaching session covers recent developments, in particular a technique used in today's strongest solvers: the alternation between "classic" depth-first search with learning, and breadth-first search for simplification.
  Bio: Dr. Marijn J.H. Heule is a Research Scientist at the University of Texas at Austin. He received his PhD at Delft University of Technology in the Netherlands in 2008. His research focuses on solving hard combinatorial problems in areas such as formal verification, number theory, and combinatorics. Most of his contributions are related to theory and practice of satisfiability (SAT) solving. He has developed award-winning SAT solvers (see http://satcompetition.org/), and his preprocessing techniques are used in most state-of-the-art SAT solvers.
• K. Rustan M. Leino (Microsoft Research, Redmond WA):
  Verified programs and proofs in Dafny
  (Dafny)
  Abstract: In these lectures, you will learn and practice the foundations of program verification, like pre- and postcondition specifications, loop invariants, termination, proofs, and induction. Dafny is a programming language that includes specifications and proof-authoring features. The lectures and labs will give you hands-on experience in using the Dafny to write and specify programs, both imperative and functional, and to write mechanically checked proofs.
  Before the Lectures: Please install Dafny on your laptop before the lectures. The binaries and plug-ins for Visual Studio and Emacs are found here: https://github.com/Microsoft/dafny

  Optional: Try out the Dafny tutorial online (http://rise4fun.com/dafny) and check out the following reading material:

  • "Dafny: An Automatic Program Verifier for Functional Correctness", K.R.M. Leino, LPAR-16, 2010.
  • "Developing Verified Programs with Dafny", K.R.M. Leino, tutorial notes ICSE 2013 (3 pages).
  • "Verified Calculations", K.R.M. Leino and N. Polikarpova, VSTTE 2013.
  • "Automating Induction with an SMT Solver", K.R.M. Leino, VMCAI 2012.

  Going beyond these lectures, the following papers describe applications of Dafny:

  • "Ironclad Apps: End-to-End Security via Automated Full-System Verification", C. Hawblitzel, J. Howell, J.R. Lorch, A. Narayan, B. Parno, D. Zhang, and B. Zing, OSDI 2014.
  • "IronFleet: proving practical distributed systems correct", C. Hawblitzel, J. Howell, M. Kapritsos, J.R. Lorch, B. Parno, M.L. Roberts, S.T.V. Setty, and B. Zill, SOSP 2015.

  Here are some texts on more advanced subjects:

  • "Automating Theorem Proving with SMT", K.R.M. Leino, ITP 2013.
  • " Well-founded Functions and Extreme Predicates in Dafny: A Tutorial", K.R.M. Leino, IWIL-2015.

  And here is some reading material that explains the technology underlying Dafny:

  • "Specification and verification of object-oriented software", K.R.M. Leino, lecture notes, Marktoberdorf International Summer School 2008.
  • "Computing with an SMT solver", N. Amin, K.R.M. Leino, and T. Rompf, TAP 2014.
  • "Trigger Selection Strategies to Stabilize Program Verifiers", K.R.M. Leino and C. Pit--Claudel, CAV 2016.
  • "Fine-grained Caching of Verification Results", K.R.M. Leino and V. Wüstholz, CAV 2015.
  Bio:

  K. Rustan M. Leino is Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond and Visiting Professor in the Department of Computing at Imperial College London. He is known for his work on programming methods and program verification tools, and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3. He is an ACM Fellow.

  Prior to Microsoft Research, Leino worked at DEC/Compaq SRC. He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft. Leino collects thinking puzzles on a popular web page and hosts the Verification Corner channel on youtube. In his spare time, he plays music and likes to cook.

• Sam Blackshear (Facebook):
  Building compositional static analyzers with Infer
  ( Infer, Lab Instructions)
  Abstract: Infer is an open-source static analysis tool used to find bugs in Java, Objective-C, and C++ code at Facebook. Recently, Infer has transitioned from a standalone separation logic-based analyzer into a general framework for quickly developing modular and compositional interprocedural analyses. The framework lifts a simple intraprocedural abstract interpreter that computes the summary for a single procedure to a compositional interprocedural analysis that scales to millions of lines of code.
  Bio: Dr. Sam Blackshear has a PhD in Compute Science from the Universit of Colorado, Boulder. He works on the Infer static analyzer at Facebook.
• Ashish Tiwari (SRI International Computer Science Laboratory):
  Formal Techniques for Analyzing Hybrid Systems
  ( Slides: Model Checking: Problem Definition, Model Checking: Example , Hybrid Systems: Definition, Model Checking: Techniques for Hybrid Systems
  Tools: SAL, HybridSAL qualitative abstractor, and HybridSAL relational abstractor )
  Abstract: Hybrid dynamical systems combine discrete state transition systems with continuous dynamical systems. They are used to model complex systems that have interacting discrete and continuous components, or systems that are broadly referred to as cyber-physical systems. This course will cover the basics of hybrid systems, and it will delve deeper into the verification problem and the various approaches for analyzing hybrid systems. The lab sessions will involve using tools for verification of hybrid systems.
  Bio: Dr. Ashish Tiwari is a senior computer scientist at SRI International. His contributions span automated reasoning, term rewriting, computer algebra, program synthesis, model checking, hybrid systems, systems biology, and cyber-physical systems.

Background Course on Logic

• Natarajan Shankar (SRI CSL) and Stéphane Graham-Lengrand (Ecole Polytechnique):
  Speaking Logic
  ( 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.

Invited Speakers

• Paolo Mancosu (UC Berkeley Philosophy):
  Assigning 'sizes' to infinite sets: some historical and systematic considerations
  Abstract: In this talk, I will give a survey of recent work I have done on the historical, mathematical, and philosophical problems related to the assignment of 'sizes' to infinite sets. I will focus in particular on infinite sets of natural numbers. The historical part of the presentation will take its start from Greek and Arabic contributions to the possibility of measuring infinite sets according to size and sketch some developments spanning the period between Galileo and Cantor. In the systematic part of the talk, I will discuss recent theories of numerosities that preserve the part-whole principle in the assignment of sizes to infinite sets of natural numbers and show how the historical and mathematical considerations yield benefits in the philosophy of mathematics. In this latter part of the talk, I will focus especially on neo-logicism.
  Bibliography: P. Mancosu, /Abstraction and Infinity/, Oxford University Press, 2017
  Bio: Paolo Mancosu is Willis S. and Marion Slusser Professor of Philosophy at the University of California at Berkeley. He is the author of numerous articles and books in logic and philosophy of mathematics. He is also the author of Inside the Zhivago Storm. The editorial adventures of Pasternak's masterpiece (Feltrinelli, Milan, 2013). During his career he has taught at Stanford, Oxford, and Yale. He has been a fellow of the Humboldt Stiftung, of the Wissenschaftskolleg zu Berlin, of the Institute for Advanced Study in Princeton, and of the Institut d'Études Avancées in Paris. He has received grants from the Guggenheim Foundation, the NSF, and the CNRS.
  
• Maria Paola Bonacina (Universita` degli Studi di Verona):
  On interpolation in theorem proving
  Abstract: An interpolant is a formula I that lies between two formulae A and B, meaning that A implies I, I implies B, and I is made of symbols that appear in both A and B. If A and B are inconsistent, a reverse interpolant is a formula I such that A implies I, and I and B are inconsistent. This lecture is an introduction to the problem of extracting a reverse interpolant from a refutation of A and B. We consider proofs by resolution in propositional logic and ground proofs in first-order logic with equality. Applications of interpolation include program analysis (e.g., abstraction refinement for model checking), program synthesis (e.g., invariant generation), and explanation of conflicts in conflict-driven satisfiability procedures.
• Vaughan Pratt (Stanford):
  Formality and rigor in treatments of global warming
  Abstract: In the early 1950s Turing and von Neumann proposed respectively chess and numerical weather prediction as applications of computers. The premise for both problems is that they are sufficiently complex that, /when suitably formalized, a sufficiently powerful computer should be able to do deal with their myriad details better than humans.

  This has recently proved to be the case for chess. However the 35 or so participants in CMIP5, the Coupled Model Intercomparison Project serving as a basis for the Fifth Assessment Report of the International Panel on Climate Change in 2013, all hindcast to 1900 poorly, raising doubts as to their ability to forecast with any usable reliability to 2100.

  In this talk we raise the possibility that climate forecasting is intrinsically harder for computers to treat as a formally stated problem amenable to raw computing power than it is for humans to treat with more conventional mathematical and statistical rigor applicable to today's data using only the computing machinery of 60 years ago, if even that. Equal time will be given to audience interaction.

Information about previous Summer Schools on Formal Techniques can be found at

• SSFT16
• SSFT15
• SSFT14
• SSFT13
• SSFT12
• SSFT11

We expect to provide support for the travel and accommodation for a limited number of students registered at US universities, but 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$600-700 for meals and lodging. Applications should be submitted at the website http://fm.csl.sri.com/SSFT17

Schedule

Applicants are urged to submit their applications before April 30, 2017, 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.

Registration is now closed

Questions on any aspect of the school can be posted here.