Third Summer School on Formal Techniques

Lectures

• Leonardo de Moura (MSR Redmond):
  Decision Methods for Arithmetic
  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.
• Cesar Munoz, (NASA Langley Research Center):
  Advanced Theorem Proving Techniques in PVS with Applications
  Abstract: The Prototype Verification System (PVS) 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.
• Aarti Gupta (NEC Labs):
  Static and Dynamic Verification of Concurrent Programs (slides, lab, ConcurrentStack.java)
  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.

• Andrey Rybalchenko (TU Munich):
  Program verification and synthesis as Horn-like constraint solving (slides, SAS 2013, CAV 2013, PLDI 2012)
  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.

• Ernie Cohen:
  Verified Programming with VCC (slides)
  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.
• Natarajan Shankar (SRI International):
  Speaking Logic (slides)
  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.
• Arnaud Venet (ARC-TI):
  Putting Numerical Abstract Domains to Work: A Study of Array-Bound Checking for C Programs (slides)
  Abstract: The inference of numerical invariants was the original application of Abstract Interpretation and remains to date its major achievement. In this lecture, we give a step-by-step description of one of the most important numerical abstract domains, the domain of convex polyhedra introduced by Cousot and Halbwachs in 1978. This domain discovers linear inequality constraints among variables of a program, which are essential to many verification tasks. We focus on a particular problem that is of great practical interest: static array-bound checking. Out-of-bounds array accesses, also known as buffer overflows, account for nearly 50% of all software vulnerabilities reported by CERT and constitute a major source of non-determinism in embedded programs. This class of errors is extremely difficult to eliminate by standard testing procedures because of its near total absence of effects on the observable behavior of programs. It is an ideal target for static analysis and, since pointer arithmetic is prevalent in C programs, numerical domains have a major role to play. We present some lessons and learning from several endeavors to effectively carry out static array-bound checking on real C code, from the mission control software of Mars Exploration Rovers to OpenSSH to auto-coded flight controllers. We describe attempts to push the scalability limits of convex polyhedra or use numerical domains that are unable to express the properties needed when applied out of the box. Despite the number of numerical domains available in the literature, there is still a need for efficient abstractions that can scale to large codes. We present a new approach to inferring linear inequality invariants, the gauge abstraction, which offers a better trade-off among expressiveness, accuracy and scalability for the purposes of array-bound checking.
• Richard Waldinger (SRI International):
  Automatic Deduction Applied: Program Synthesis and Question Answering. (slides)