21-26 May 2017
Atherton CA, U.S.A.
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.
--
[LOGIC] mailing list
http://www.dvmlg.de/mailingliste.html
Archive: http://www.illc.uva.nl/LogicList/
provided by a collaboration of the DVMLG, the Maths Departments in Bonn and Hamburg, and the ILLC at the Universiteit van Amsterdam