Seventh Summer School on Formal Techniques, May 21-26, 2017, Menlo College, Atherton

[Sam Owre]

Seventh Summer School on Formal Techniques, May 21 - May 26, 2017,
Menlo College
Atherton, California
http://fm.csl.sri.com/SSFT17

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)

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 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:

*  Stephanie Delaune (IRISA France):
   Verification of security protocols: from confidentiality to privacy
   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.

*  Marjijn Heule (University of Texas at Austin):
   State-of-the-art SAT Solving
   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.

*  K. Rustan M. Leino (Microsoft Research, Redmond WA):
   Verified programs and proofs in 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.

*  Sam Blackshear (Facebook):
   Building compositional static analyzers with Infer
   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.

*  Ashish Tiwari (SRI International Computer Science Laboratory):
   Formal Techniques for Analyzing Hybrid Systems
   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.

The main lectures in the summer school will be preceded by a background
course on logic taught by Natarajan Shankar (SRI)and Stephane
Graham-Lengrand (Ecole Polytechnique) on

* 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.

Note: The school is preceded by the 9th NASA Formal Methods Symposium
(NFM) 2017 (https://ti.arc.nasa.gov/events/nfm-2017/) and the associated
sixth Automated Formal Methods (AFM) 2017 (http://fm.csl.sri.com/AFM17/)
workshop. On May 20 there will be an AFM tutorial day that students are
encouraged to attend.

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

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 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, 2016,
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.