[TYPES/announce] Third Summer School on Formal Techniques, May 20-24, 2013, Atherton, California

[Natarajan Shankar]

Third Summer School on Formal Techniques
May 20 - May 24, 2013
Menlo College, Atherton, CA
http://fm.csl.sri.com/SSFT13

Follows VSTTE May 17-19 in the same location:
https://sites.google.com/site/vstte2013/

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
          http://fm.csl.sri.com/SSFT13

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