Second Summer School on Formal Techniques
May 27 June 1, 2012
Menlo College, Atherton, CA
Formal verification techniques such as model checking, satisfiability, and
static analysis have matured rapidly in recent years. This school, the
second in the series, will focus on the principles and practice of formal
verification, 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 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) was held in May 2011. This year, the
school starts on Sun May 27 with a background course on Logic in Computer
Science taught by Natarajan Shankar (SRI). The course is optional but
highly recommended  it covers the prerequisites for the main lectures.
N. Shankar:
Speaking Logic
Lectures

Leonardo de Moura (MSR Redmond) and Bruno Dutertre (SRI):
Satisfiability Modulo Theories
[Slides:
Introduction,
Theory Solving,
Quantifiers,
Applications]
Abstract: We present an overview of the theory and practice of
satisfiability solving modulo theories (SMT), covering the basics
of propositional satisfiability, theoryspecific solvers, and their
integration into an SMT solver; the effective ways of applying
SMT technology in formal verification and constraint solving; and
the current research challenges in scaling SMT technology to handle
larger problems and a broader range of problems.

Sumit Gulwani (MSR):
Dimensions in Program Synthesis
[Slides: Lecture 1
(ppt),
(pdf),
Lecture 2
(ppt),
(pdf),
Lecture 3
(ppt),
(pdf)]
Abstract: Program Synthesis is the task of searching for a
program in some underlying domain that matches the user's intent. These
lectures will describe three key dimensions in program synthesis: (a)
User Interaction Model: The user may specify the intent using examples,
demonstrations, logical specifications, keywords, natural language,
sketch, or partial/inefficient programs. A key challenge here is to
design a user interactional model that can deal with inherent
ambiguities in underspecification (b) Search technique: We will cover
techniques that have been developed in various communities including use
of SAT/SMT solvers (formal methods community), version space algebras
(machine learning community), and A*style goaldirected heuristics (AI
community). (c) Underlying domain of programs that can range from
straightline programs to programs with restricted form of
loops/conditionals/events. These concepts will be illustrated via a
variety of applications in algorithm/software development (e.g.,
Bitvector algorithms, Program inverses) and enduser programming (e.g.,
Spreadsheet/drawing macros, Smartphone scripts). We will also present
some surprising applications in the area of automating education
including solution generation, problem generation, automated grading,
and content creation in a variety of math and science domains.

Daniel Kroening (Oxford):
Verifying Concurrent Programs
[Slides: Verifying Concurrent Programs,
Predicate Abstraction]
Abstract: Concurrent software model checking is one of the most
challenging problems facing the verification community today. Not only
does software generally suffer from data state explosion. Concurrent
software in particular is susceptible to state explosion due to the need
to track arbitrary thread interleavings, whose number grows
exponentially with the number of executing threads.
Predicate abstraction was introduced as a way of dealing with data state
explosion: the program state is approximated via the values of a finite
number of predicates over the program variables. Predicate abstraction
turns C programs into finitestate Boolean programs, which can be model
checked. Predicate abstraction is typically embedded into a
counterexampleguided abstraction refinement (CEGAR) framework. The
feasibility of the overall approach was convincingly demonstrated for
sequential software by the success of the SLAM project at Microsoft,
which was able to discover numerous controldominated errors in
lowlevel operating system code. We will provide an introduction to
predicate abstraction, CEGAR, and then discuss the extensions required
to deal with concurrent software.

Ken McMillan:
Abstraction, Decomposition, and Relevance
Abstract: Proofs of large and complex systems can be daunting.
We can make complex proofs manageable by a process of decomposition and
abstraction. We first break the proofs of the system's specification down
into a collection of simpler properties. Then for each property, we
abstract away details about the system that are not relevant to that
particular property, thus simplifying the proof effort. In these lectures
we will consider:
 How to decompose large proofs into simple properties
 How to apply abstraction to eliminate irrelevant detail
 How to determine automatically what information is relevant to a given property.
We will see that the problem of relevance can be approached by generalizing
from particular cases, applying the principle of Occam's razor. This idea will
be illustrated using a method called Craig Interpolation that allows us to
construct simple proofs in various forms that abstract away from irrelevant detail.

Corina Pasareanu, Dimitra Giannakopoulou, Neha Rungta, Peter Mehlitz,
and Oksana Tkachuk:
Verifying Components in the Right Context
[slides: (Pasareanu): Compositional Verification,
(Mehlitz,Tkachuk): PathFinder Part 1,
Part 2,
Part 3]
Abstract: Model checking is typically applied to the verification
of critical components in large systems. However, components are
fundamentally "open"; their behavior is dependent on the environment in
which they operate, i.e., on the external events and on values defined
outside the component but referenced inside. A key challenge in
component verification is modeling the component environment. In
particular, a good environment model (the "right context") should enable
sufficiently precise yet tractable verification.
We will present techniques for automatically creating component
environments, including abstraction and learning approaches, among
others. We will discuss environment implementations based on various
formalisms, ranging from event scripting languages and framework
abstractions, to temporal logic specifications and finite state
automata. Environment modeling and component verification will be
illustrated within the Java PathFinder verification toolset.
Invited Talks

Aaron Bradley:
IC3 and Beyond: Incremental, Inductive Verification
[Slides: IC3]
Abstract: In "Temporal Verification of Reactive Systems: Safety," Zohar Manna
and Amir Pnueli discuss two strategies for strengthening an invariant
property to be inductive: "(1) Use a stronger assertion, or (2)
Conduct an incremental proof, using previously established
invariants." They "strongly recommend" the use of the second approach
"whenever applicable," its advantage being "modularity." Yet they
note that it is not always applicable, as a conjunction of assertions
can be inductive while none of its components, on its own, need be
inductive. In manual proofs, an experienced verifier follows this
recommendation by iterating the following steps until a complete proof
is discovered: first, identify a reason why the current lemmas are
insufficient to prove the desired property; second, develop a new
lemma to address that reason.
However, until IC3, successful algorithmic approaches to model
checking followed the first approach. For example, kinduction
strengthens the property by unrolling; an interpolating model checker
iterates an interpolantbased approximate postimage computation until
convergence, refining through further unrolling. While both rely on
the conflictclause learning of the underlying SAT solver, neither use
induction to discover intermediate lemmas as Manna and Pnueli
recommend. Only their ultimate convergence relies on induction.
IC3 was a result of asking the question: if an incremental strategy is
better for humans, might it not be better for algorithms as well? The
fundamental issue in applying the second approach directly, though, is
the situation in which two or more essential lemmas are mutually
inductive but not independently so. They must be discovered together.
IC3 addresses this problem by introducing stepwiserelative inductive
lemma generation: if the reason that the current lemma set is
insufficient cannot be addressed with an inductive lemma, address it
with a lemma that holds for a certain number of transitions, and keep
looking. IC3 thus smoothly transitions between Manna's and Pnueli's
second approach, when possible, and their first approach, when
necessary.
In this talk, we discuss how incremental, inductive verification (IIV)
has motivated new algorithms for model checking safety properties
(IC3), omegaregular properties (FAIR), and CTL properties (IICTL).

Alex Aiken:
New Applications of Underapproximations in Static Analysis

Dawn Song:
BitBlazeWebBlazeDroidBlaze: Automatic Security
Analysis in Binary, Web and Android
Abstract: I will present the BitBlaze project, describing how
we build a unified binary program analysis platform and use it to
provide novel solutions to computer security problems, including
automatic vulnerability discovery and defense, indepth malware
analysis, and automatic extraction of
security models for analysis and verification. The BitBlaze Binary
Analysis Infrastructure is a fusion of static and dynamic analysis
techniques and enables a set of powerful, novel symbolic reasoning
techniques on program binaries. I will also talk about BitTurner,
the first public cloudbased
service for automatic test case generation and security audit powered
by dynamic symbolic execution on program binaries.
I will give an overview of the WebBlaze project, aiming at designing
and developing new techniques and tools to improve web
security, including automatic dynamic symbolic execution on JavaScript
for indepth vulnerability detection in rich web applications.
Finally, I will describe some ongoing efforts in DroidBlaze, an
automatic security analysis infrastructure for Android apps.
More information about BitBlaze and WebBlaze is available at
http://bitblaze.cs.berkeley.edu
and http://webblaze.cs.berkeley.edu.
Registration is now closed
Questions on any aspect of the school can be posted
here.
>