[FM-India] Third Summer School on Formal Techniques

Madhavan Mukund madhavan at cmi.ac.in
Wed May 1 22:04:24 IST 2013

 From: "Rungta, Neha S. (ARC-TI)[Stinger Ghaffarian Technologies Inc. (SGT
  Inc.)]" <neha.s.rungta at nasa.gov>
 To: "fm-announcements at lists.nasa.gov" <fm-announcements at lists.nasa.gov>
 Date: Wed, 1 May 2013 09:55:55 -0500
 Subject: [fm-announcements] Third Summer School on Formal Techniques
 Third Summer School on Formal Techniques
 May 20 - May 24, 2013
 Menlo College, Atherton, CA
 Follows VSTTE May 17-19 in the same location:
 Formal verification techniques such as model checking, satisfiability, and
 static analysis have matured rapidly in recent years. This school, the
 third in the series, will focus on the principles and practice of formal
 verification, 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 using verification technology in their
 own research in computing as well as engineering, biology, and
 mathematics. Students at the school will have the opportunity to
 experiment with the tools and techniques presented in the lectures.
 The first Summer Formal school (SSFT11; http://fm.csl.sri.com/SSFT11) was
 held in May 2011 and the second (SSFT12; http://fm.csl.sri.com/SSFT12) was
 held in May 2012.
 We have NSF support for the travel and accommodation for students from US
 universities, but welcome applications from graduate students at non-US
 universities as well. Non-US students will have to cover their travel and
 lodging expenses (around $500). The deadline for applications is April
 30. Non-US students requiring US visas are requested to apply early (by
 April 15).  Interested students can submit their application at
 The lectures at the school include:
 Title: Decision Methods for Arithmetic
 Lecturer: Leonardo de Moura, Microsoft Research
 Abstract: Decision methods for arithmetic are extensively used in the
 formal verification and analysis of software and cyber-physical
 systems, computer algebra, and formalized mathematics. In these talks,
 we will cover several decision methods for fragments of arithmetic
 such as the elementary theories of algebra and geometry over the Real
 and Complex numbers. We will also describe the general techniques used
 in the design of these procedures: saturation, model-based methods,
 abstract/refine loop, infinitesimals, etc.  We assume only a basic
 grounding in first-order logic.
 Title: Advanced Theorem Proving Techniques in PVS with Applications
 Lecturer: Cesar Munoz, NASA Langley Research Center Hampton, VA
 23681-2199, USA
 Abstract: The Prototype Verification System (PVS)
 [http://pvs.csl.sri.com<http://pvs.csl.sri.com/>] is an interactive environment for the
 specification and verification of systems. PVS provides a strongly
 typed specification language, which is based on Higher-Order
 Logic. The type system of PVS supports: sub-typing, dependent-types,
 abstract data types, parametric types, records, unions, and
 tuples. The PVS theorem prover includes decision procedures for a
 variety of theories such as linear arithmetic, propositional logic,
 and temporal logic.  This seminar will provide a gentle introduction
 to advanced PVS features, including types for specifications, implicit
 induction, iterations, rapid prototyping, strategy writing, and
 computational reflection.
 Title: Static and Dynamic Verification of Concurrent Programs
 Lecturer: Aarti Gupta, NEC Labs
 Abstract: The need to harness the computing power of modern multi-core
 platforms has driven a resurgence of interest in concurrent
 programs. However, it is very challenging to develop correct
 concurrent programs, and in practice programs often exhibit bugs
 related to subtle synchronization effects. These lectures will
 describe various static and dynamic techniques underlying automatic
 verification and debugging of concurrent programs. The emphasis will
 be on main ideas to reason about synchronizations and interleavings
 between interacting threads or processes.
 On the static side, we first review some theoretical results on model
 checking based on interacting pushdown system (PDS)
 models. Decidability results here limit the patterns of
 synchronization allowed. Next, we consider the practice of model
 checking concurrent programs, where the main challenge is in managing
 the explosion in interleavings. We consider both explicit and symbolic
 state space exploration, where various techniques are inspired by
 successful verification of finite state systems on one hand, and
 sequential programs on the other.
 Due to scalability limitations of static verification, there has been
 increased interest in dynamic techniques for systematically exploring
 (parts of) concurrent programs. We discuss preemptive context bounding
 techniques that control the scheduler to dynamically explore other
 interleavings. We also consider predictive analysis techniques, where
 a trace-based model derived from dynamic executions is used to predict
 concurrency bugs.
 Title: Program verification and synthesis as Horn-like constraint solving
 Lecturer: Andrey Rybalchenko, TU Munich
 Abstract: First, we review how proving reachability and termination
 properties of transition systems, procedural programs, multi-threaded
 programs, and higher- order functional programs can be reduced to
 constraint solving for Horn-like constraints.  This step will cover
 properties over program variables of scalar and array data types.
 Second, we show how universal and existential temporal properties can
 be proved using contraint-based setting equipped with existential
 quantification.  Third, we present a reduction from reactive program
 synthesis to existentially quantified Horn-like constraints. Finally,
 we discuss adequate solving algorithms and tools.
 The material would cover/export syntax and semantics of Horn clauses
 over theory literals, basics of temporal proof rules for reasoning
 about programs, basics of CTL and synthesis together with deductive
 proof rules, bottom-up inference/ resolution of Horn clauses,
 Skolemization, abstraction, interpolation.
 Title: Verified Programming with VCC
 Speaker: Ernie Cohen
 Abstract: In the last few years it has become practical to write
 real-world code and prove that it meets its specifications. This
 course provides an introduction to the joys of verified programming
 using VCC, a deductive verifier for concurrent C code.
 Title: Speaking Logic
 Speaker: Natarajan Shankar, SRI International
 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.

More information about the FMIndia mailing list