Seventh Summer School on Formal Techniques
May 21 - May 26, 2017
Menlo College, Atherton, CA
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.
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
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.
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),
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.
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
K. Rustan M. Leino (Microsoft Research, Redmond WA):
Verified programs and proofs in Dafny
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
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
- "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 Veriﬁers", K.R.M. Leino and C. Pit--Claudel, CAV 2016.
- "Fine-grained Caching of Veriﬁcation Results", K.R.M. Leino and V. Wüstholz, CAV 2015.
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)
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.
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
Model Checking: Problem Definition,
Model Checking: Example ,
Hybrid Systems: Definition,
Model Checking: Techniques for Hybrid Systems
qualitative abstractor, and
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.
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):
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.
Paolo Mancosu (UC Berkeley Philosophy):
Assigning 'sizes' to infinite sets: some historical and
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
P. Mancosu, /Abstraction and Infinity/, Oxford University Press, 2017
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
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
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
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
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.
Questions on any aspect of the school can be posted
†NOTE: Underrepresented minority
refers to African Americans, Mexican-Americans, Native Americans
(American Indians, Alaska Natives, and Native Hawaiians),
Pacific Islanders, and mainland Puerto Ricans.