Sixth Summer School on Formal Techniques
May 22  May 27, 2016
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 sixth in the series,
will focus on the principles and practice of formal techniques, with a
strong emphasis on the handson 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.
Background Course on Logic

Natarajan Shankar (SRI CSL) and Stéphane GrahamLengrand (Ecole Polytechnique):
Speaking Logic
(
Speaking Logic,
Type Theory,
Coq Files,
Reading,
PVS Course,
PVS
)
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.
Lecturers
Clark Barrett (NYU/Stanford), Stefano Tonetta (FBK Italy),
JeanChristophe Filliatre (LRI Paris), Carolyn Talcott (SRI),
and Natarajan Shankar (SRI)

Clark Barrett (NYU/Stanford):
Satisfiability Modulo Theories
(Slides)
Abstract:
I will give an introduction to Satisfiability Modulo Theories (SMT)
solvers, including the DPLL(T) architecture that combines a Boolean
satisfiability (SAT) solver with a theory solver, techniques for
building individual theory solvers, and techniques for theory
combination. Lab sessions will explore these ideas by building and
experimenting with small modules within the CVC4 SMT solver.

Stefano Tonetta^{†} (FBK Italy):
Advanced model checking for verification and safety assessment
(Slides)
Abstract:
The course will review the recent developments in model checking for
finite and infinitestate transition systems, including IC3 and its
integration with implicit abstraction. We will then present a formal
approach to contractbased refinement, and will cover the problem of
safety analysis, i.e. assessing the response of a system to faults by
automatically generating Fault Trees. We will report the results on
two recent case studies on the application of these techniques: the
AIR6110 Wheel Brake System, and the NextGen protocol.
The practical sessions will rely on the use of the nuXmv model
checker, the xSAP platform for safety analysis, and the OCRA system
for contract refinement.

JeanChristophe Filliatre (ParisSud, CNRS):
An Introduction to Deductive Program Verification
(Materials)
Abstract:
This lecture introduces elementary concepts and techniques related to
deductive program verification, such as loop invariants, function
contracts, termination proofs, ghost code, modeling of data
structures, weakest preconditions, etc. A particular focus is made on
the use of automated theorem provers in the verification process and
the tension that may exists between an elegant specification and a
fully automated proof. The lecture includes many examples using the
Why3 tool (http://why3.lri.fr/) and lab sessions will invite
participants to formally verify small yet challenging programs using
Why3.

Carolyn Talcott (SRI International Computer Science Laboratory):
Pathway Logic: Using Formal Techniques to Understand How Cells Work
(
Slides,
Exercises,
Maude)
Abstract:
Pathway Logic (PL) is a framework based on rewriting logic for
developing and analyzing formal executable models of cellular
processes. The long term objective is better understanding of how
cells work. Progress towards this goal involves curation of
experimental knowledge, assembly of models to study a question of
interest, visualizing the resulting models and using formal reasoning
techniques to determine properties predicted by the models.
In these lectures we will focus on signal transduction: how cells
sense their external and internal environment and make decisions. We
will begin with some background and describe the informal models and
reasoning often used by biologists. We will describe the PL
representation of cellular signaling systems as rewriting logic
specifications (using the Maude language). We will explain how
knowledge is curated as formal objects, called datums, representing
experimental findings, and the logic used to infer rewrite rules from
datums. We will then introduce the Pathway Logic Assistant (PLA) a
tool for interacting with PL knowledge bases. Using PLA one can search
a knowledge base or assemble and visualize a model. Once a model is
assembled one can explore its structure or ask questions such as `how
can a given state be reached?' (the answer is an execution pathway) or
`what if I remove this or add that?'. PLA treats signaling models as
models of (tiny) distributed systems and using formal techniques such
as forward/backward collection, search, and model checking to answer
questions. We will briefly look under the hood of PLA to see how
reflection is used to enable Maude to be part of an interactive
system. Reflection is also used to manage multiple representations of
the knowledge base and derived models for export/import to integrate
with other tools and knowledge bases, for example graph drawing tools
or special purpose model checkers.
The features of PL and PLA will be illustrated with substantial case
studies.

Sam Owre and Natarajan Shankar (SRI International Computer Science Laboratory):
Specification, Verification, and Interactive Proof
(
Slides,
PVS Files,
Exercises,
PVS)
Abstract:
Formalization plays a key role in computing in disciplines ranging
from hardware and distributed computing to programming languages and
hybrid systems. In this course, we explore the use of SRI's Prototype
Verification System (PVS)[http://pvs.csl.sri.com] in formal
specification and interactive proof construction. PVS and other proof
assistants like ACL2, Coq, HOL, HOL Light, Isabelle, and Nuprl, have
been used to formalize significant tracts of mathematics and verify
complex hardware and software systems. In the lectures, we will
explore the formalization of both introductory and advanced concepts
from mathematics and computing. In the lab sessions, we use PVS to
interactively construct proofs and to define new proof strategies.
Invited Speakers

Johan van Benthem^{‡} (Stanford/CWI):
Logic, Games, and Computation
Abstract:
Logic and human agency form a natural field of investigation, and have
done so ever since logic started. Influences from many disciplines meet
at this interface today, ranging from philosophy to computer science,
economics, and cognitive science. I will discuss some major current
themes in logic and agency, using games as a unifying paradigm.
I will give examples of how logic can be used to analyze games,
but also how games can be used to analyze logic, and finally,
how both directions connect with the foundations of computation.
I end with some basic open problems that face us in this setting.

Cindy Rubio Gonzalez (UC Davis):
FloatingPoint Precision Tuning Using Blame Analysis
Abstract:

Maria Paola Bonacina (Università degli Studi di Verona):
Orderingbased Strategies for Theorem Proving
(
Slides)
Abstract:
After a brief presentation of automated reasoning as a field
of computer science, the lecture focuses on firstorder logic
as a machineoriented language and surveys orderingbased
strategies for firstorder theorem proving. It covers some of
the basic building blocks of a theorem prover, illustrating
both inference and search aspects, and conveying that reasoning
is about ignoring what is redundant as much as it is getting
what is relevant.
^{† Alessandro Cimatti is unable to lecture at the
summer school. Professor Stefano Tonetta (FBK Italy) has kindly
agreed to take his place.↩}
^{‡ Professor Sol Feferman is unable to present a
lecture. We are pleased to announce that Professor Johan van Benthem
(Amsterdam and Stanford) has kindly agreed to lecture in his place.↩}
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 nonUS students as well as nonstudents (if space
permits). NonUS 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/SSFT16
Applicants are urged to submit their applications before April 30,
2016, since there are only a limited number of spaces available.
NonUS applicants requiring US visas are requested to apply early. We
strongly encourage the participation of women and underrepresented
minorities in the summer school.
Registration is now closed
Questions on any aspect of the school can be posted
here.
^{†}NOTE: Underrepresented minority
refers to African Americans, MexicanAmericans, Native Americans
(American Indians, Alaska Natives, and Native Hawaiians),
Pacific Islanders, and mainland Puerto Ricans.
Questions and Answers