[TYPES/announce] Sixth Summer School on Formal Techniques, May 22 - 27, 2016, Atherton California

Tue Apr 5 08:35:32 EDT 2016

   Sixth Summer School on Formal Techniques, May 22 - May 27, 2016,
   Menlo College
   Atherton, California
   http://fm.csl.sri.com/SSFT16

Lecturers: Carolyn Talcott (SRI), Jean-Christophe Filliatre (LRI Paris),
            Alessandro Cimatti (FBK Trento), Clark Barrett (NYU/Stanford),
            Stephane Graham-Lengrand (Ecole Polytechnique),  Sam Owre (SRI),
            and Natarajan Shankar (SRI)

Invited Speakers:
   Sol Feferman (Stanford): A logical framework for mathematical practice
   Maria Paola Bonacina (Universita degli Studi di Verona):
                            Ordering-based strategies for theorem proving
   Cindy Rubio Gonzalez (University of California, Davis):
                            Floating-Point Precision Tuning Using Blame 
Analysis

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

The lecturers at the school include:

* Clark Barrett (NYU/Stanford)
   Satisfiability Modulo Theories

   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.

* Alessandro Cimatti (FBK Trento)
   Advanced model checking for verification and safety assessment

   The course will review the recent developments in model checking for
   finite- and infinite-state transition systems, including IC3 and its
   integration with implicit abstraction. We will then present a formal
   approach to contract-based 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.

* Jean-Christophe Filliatre (Paris-Sud, CNRS)
   An Introduction to Deductive Program Verification

   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)
   Title: Pathway Logic:  Using Formal Techniques to Understand How 
Cells Work
   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

   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://fm.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.

==================================================================

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

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/SSFT16

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.