[TYPES/announce] Seventh Summer School on Formal Techniques, May 21 - May 26, 2017, Atherton, California

[Natarajan Shankar]

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