Second Summer School on Formal Techniques

Schedule

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, theory-specific 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 under-specification (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 goal-directed heuristics (AI community). (c) Underlying domain of programs that can range from straight-line 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 end-user 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 finite-state Boolean programs, which can be model checked. Predicate abstraction is typically embedded into a counterexample-guided 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 control-dominated errors in low-level 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 tool-set.

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, k-induction strengthens the property by unrolling; an interpolating model checker iterates an interpolant-based approximate post-image computation until convergence, refining through further unrolling. While both rely on the conflict-clause 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 stepwise-relative 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), omega-regular properties (FAIR), and CTL properties (IICTL).

• Alex Aiken:
  New Applications of Underapproximations in Static Analysis
• Dawn Song:
  BitBlaze-WebBlaze-DroidBlaze: 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, in-depth 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 cloud-based 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 in-depth 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