[SMT-LIB] Fifth Summer School on Formal Techniques, May 17 - May 22, 2015, Atherton, California

[Natarajan Shankar]

Fifth Summer School on Formal Techniques
May 17 - May 22, 2015
Menlo College, Atherton, CA
http://fm.csl.sri.com/SSFT15

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

* Arie Gurfinkel (SEI CMU, USA):
     Building Program Verifiers from Compilers and Theorem Provers

Abstract: Developing an automated program verifier is an extremely difficult
task. By its very nature, a verifier shares many of the complexities of an
optimizing compiler and of an efficient automated theorem prover. From the
compiler perspective, the issues include idiomatic syntax, parsing, 
intermediate
representation, static analysis, and equivalence preserving program
transformations. From the theorem proving perspective, the issues include
verification logic, verification condition generation, synthesizes of 
sufficient
inductive invariants, deciding satisfiability, interpolation, and 
consequence
generation. Luckily, the cores of both compilers and theorem provers are 
well
understood, well-defined, and readily available. In these lectures, we 
examine how
to build a state-of-the-art program verifier by re-using much of existing
compilers and SMT-solvers. The lectures are based on the SeaHorn 
verification
framework developed at CMU.

* Cathy Meadows (NRL, USA):
     Cryptographic Protocol Analysis Modulo Equational Theories: the 
Maude-NRL Protocol Analyzer

Abstract: In this course we give an overview of the Maude-NPA Protocol
Analyzer. Maude-NPA is a tool for the symbolic analysis for cryptographic
protocols. It searches for ways in which an active attacker could 
subvert the
protocols' goals, such as authentication or secrecy. Maude-NPA is 
designed to take
account of the algebraic properties of the crypto systems involved, in 
order to
give a more complete representation of both the protocol and the attacker's
capabilities. We give a presentation of the theory and principles under 
which
Maude-NPA operates, and also give the students the opportunity to gain 
hands-on
experience with the tool.

* Bart Jacobs (KU Leuven, Belgium):
     VeriFast: Modular verification of sequential and concurrent C and 
Java programs
               using separation logic

Abstract: VeriFast is a tool that takes as input a C or Java program module
annotated with preconditions, postconditions, loop invariants, data 
structure
descriptions and proof hints written in a variant of separation logic, and,
without further user interaction and usually in a matter of seconds, returns
either "0 errors found", or a failed symbolic execution path. If the 
tool reports
"0 errors found" for all modules of a program, this means no execution 
of the
program accesses unallocated memory, performs a data race, or violates 
any of the
user-specified assertions. The tool operates by symbolically executing each
function/method, using a separation logic formula to represent the state of
memory, and using an SMT solver to decide proof obligations about data 
values.

In these lectures, you will learn how to use VeriFast to modularly verify
sequential and concurrent C and Java programs, and you will also learn how
VeriFast operates internally, and why, if it reports "0 errors found", 
the program
does indeed satisfy the specified properties.

* Kim Guldstrand Larsen (Aalborg University, Denmark):
     From Timed Automata to Stochastic Hybrid Games
     -- Model Checking, Performance Evaluation and Synthesis

Abstract: Timed automata and games, priced timed automata and energy 
automata have
emerged as useful formalisms for modeling real-time and energy-aware 
systems as
found in several embedded and cyber-physical systems. During the last 20 
years the
real-time model checker UPPAAL has been developed allowing for efficient
verification of hard timing constraints of timed automata. Moreover a 
number of
significant branches exists, e.g. UPPAAL CORA providing efficient 
support for
optimization, and UPPAAL TIGA allowing for automatic synthesis of 
strategies for
given safety and liveness objectives. Most recently, the branch UPPAAL 
SMC, a
highly scalable new engine has been released supporting (distributed) 
statistical
model checking (and synthesis) of stochastic hybrid automata (and games).

The lecture will review the various branches of UPPAAL and their concerted
applications to a range of real-time and cyber-physical examples including
schedulability and performance evaluation of mixed criticality systems, 
modeling
and analysis of biological systems, energy-aware wireless sensor 
networks, smart
grids and energy aware buildings and battery scheduling. Also, we shall 
see how
other branches of UPPAAL may benefit from the new scalable engine of 
UPPAAL SMC in
order to improve their performance as well as scope in terms of the 
models that
they are supporting. This includes application of UPPAAL SMC to counter 
example
generation, refinement checking, controller synthesis, and optimization.

The lab sessions will be based on exercises requiring hands-on 
experience with
UPPAAL, UPPAAL TIGA and UPPAAL SMC (all down-loadable from www.uppaal.org).

* John Harrison, Intel (Portland, USA):
     HOL Light --- from foundations to applications

Abstract: The HOL Light theorem prover is a real-world theorem proving 
program
with an unusually simple logical kernel. It has been used both for 
applictions in
formal verification, especially of floating-point algorithms, and pure 
mathematics
including the Flyspeck project's formal proof of the Kepler conjecture. 
We will
describe how the system is built up from its low-level foundations and 
how it can
be applied in various areas.

* Natarajan Shankar (SRI CSL):
     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.

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

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$550 for meals and 
lodging.
Applications should be submitted at the website http://fm.csl.sri.com/SSFT15

Applicants are encouraged to submit their applications before April 30, 
2015,
since there are only a limited number of spaces available.  Non-US 
applicants
requiring US visas are requested to apply early.