SYNASC Tutorials on Software Verification and Theorem Proving
Two-day programme of four tutorials on September 28-29.
- SMT-solvers and Theorem Proving;
- Software Verification (Safety, Reachability, Termination)
- Andrey Rybalchenko (Max Planck Institute for Software Systems, Germany)
Title: "Automated methods for proving program termination and liveness"
Abstract: Termination and liveness properties ensure that programs do not freeze and deliver requested results, e.g., a callback function terminates or a requested resource is eventually provided a managing routine. We will present algorithms and tools for the automated verification of termination and liveness properties of programs. The tutorial will present classical and recently developed methods for proving program termination based on ranking functions and transition invariants. The main focus will be on the synthesis algorithms and abstraction techniques. We will also briefly discuss methods for dealing with liveness properties.
- Nikolaj Bjorner (Microsoft Research, Redmond, US)
Title: "SMT solvers for Testing, Program Analysis and Verification at Microsoft"
Abstract: Decision procedures for checking satisfiability of logical formulas are crucial for many testing, program analysis and verification applications. Of particular recent interest are solvers for satisfiability Modulo Theories (SMT). SMT solvers are theorem provers that allow combining specialized algorithms for checking satisfiability from different domains. This tutorial is centered around the Microsoft SMT solver, Z3. We will describe how SMT solvers, and Z3 in particular, are used in program analysis and verification. Several concrete applications from program analysis at Microsoft will be presented. These applications include dynamic-symbolic test-case generation tools SAGE and Pex, they include the static analysis tools Havoc and the well-established tool PREfix which is used on most Microsoft code bases prior to shipping, and they include the program verification tools Spec#/Boogie and the C verification system, VCC, currently used on the Viridian Hypervisor. We will also give an introduction on the theory behind these solvers. We will describe the key techniques that were used for bridging the program test/analysis and verification domains into the SMT solver and some of the theory that was crucial for building an industrial-strength solver.
By attending this tutorial, the audience will get a better understanding of the challenges and symbolic solver techniques currently used in some of the software analysis tools developed at Microsoft Research.
- Helmut Veith (Technical University of Darmstadt, Germany)
Title: "Automated Software Analysis"
Abstract: Recent years have seen tremendous progress in the capabilities
of software model checkers. These tools are the result of combined
efforts by different communities, most notably model checking, abstract
interpretation, program semantics, and decision procedures. In this
tutorial, we will introduce the fundamentals of software model checking,
and show how the different origins of the field combine to a common
Duration: 2 x 1.5h (28 September, 9:00-12:30)
- Andrei Voronkov (University of Manchester, UK)
Title: "Satisfiability and Theories"
Abstract: We give a simple introduction to satisfiability modulo theories intended for non-specialists. No previous background is assumed. We will cover the following topics:
(1) Propositional satisfiability
(2) DPLL - the method for satisfiability checking
(3) Implementation of DPLL
(5) Satisfiability modulo theories
(6) Decision procedures for theories
(7) Satisfiability in a combination of theories
Instead of proving theorems, we will try to explain the main ideas using examples.
Duration: 2 x 1.5 h (28 September, 14:00-17:20)