[FM-India] Fifth Summer School on Formal Techniques, CA

[Madhavan Mukund]

 Date: Wed, 11 Mar 2015 16:41:04 +0000
 From: "Rungta, Neha S. (ARC-TI)[SGT, INC]" <neha.s.rungta at nasa.gov>
 To: "fm-announcements at lists.nasa.gov" <fm-announcements at lists.nasa.gov>
 Subject: [fm-announcements] Fifth Summer School on Formal Techniques, CA
 
 Fifth Summer School on Formal Techniques, May 17 - May 22, 2015, Atherton, California
 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 applications 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. In the lab exercises we will try to show not only how
 to perform basic formal proofs, but how conceptually simple it is to add new
 "correct by construction" derived rules of inference.
 
 * 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 urged 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.  We strongly encourage the participation of
 women and under-represented minorities in the summer school.
 ---