The school’s theme for 2013 was Program Analysis and Verification, in connection with the action line SciLex of DigiCosme. Four speakers presented several aspects of this theme, including abstract interpretation, analysis of numerical precision, model-based testing, deductive program verification, verification of protocols, construction of certified program analyzers.
Lecturers, Courses and Schedule
|Monday 22||Tuesday 23||Wednesday 24||Thursday 25||Friday 26|
|09:00-10:30||Lecture 2||Lecture 3||Lecture 4||Lecture 5|
|11:00-12:30||Lecture 2||Lecture 3||Lecture 4||Lecture 5|
|14:30-16:00||Lecture 1||Lecture 3||Lecture 4||Lecture 5|
|16:30-18:00||Lecture 1||Lecture 3||Lecture 4||Lecture 5|
- Lecture 1 Jean-Christophe Filliâtre, LRI, CNRS & University Paris-Sud, Orsay, France. Deductive Program Verification with Why3 This lecture is an introduction to deductive program verification and to the tool Why3 (http://why3.lri.fr/). This tool provides an imperative programming language (with polymorphism, algebraic data types, pattern matching, exceptions, references, arrays, etc.), a specification language that is an extension of first-order logic, and a technology to verify programs using interactive and automated theorem provers (Coq, Alt-Ergo, Z3, CVC3, etc.). Through many examples, this lecture introduces elementary concepts of program verification (pre- and postconditions, loop invariants, variants, ghost code, etc.) as well as techniques (specification, termination proofs, modeling of data structures, etc.).
- Lecture 2 Burkhart Wolff, LRI, CNRS & University Paris-Sud, Orsay, France. Model-based Testing with Isabelle-HOL-TestGen Many testing techniques vitally depend on symbolic computation and constraint-solving techniques. Their limits therefore represent limits for testing as a whole. The HOL-TestGen system is designed as plug-in into the state-of-the-art theorem proving environment Isabelle/HOL. Thus, powerful modeling languages as well as powerful automated and interactive proof methods for constraint resolution are available. HOL-TestGen has been applied in unit, sequence, and reactive sequence black-box test scenarios in substantial case studies. Conceptually, it offers a quite unique combined view on these areas traditionally considered separately. Moreover, it bridges the gap to traditional program verification by concepts such as ‘explicit test hypothesis’. The tutorial is going to be a guided tour through theory, pragmatics, and case-studies.
- Lecture 3 Cédric Fournet, Microsoft Research, Cambridge, UK. Verification of protocols and of their implementations
- Lecture 4 Sylvie Putot, CEA-List & Ecole Polytechnique, Palaiseau, France. Static analysis of numerical programs and systems Proving the software reliability of safety-critical embedded systems is a major challenge in our era, where numerical computing is becoming more and more important. In this course, we will present abstract interpretation based methods for the static analysis of numerical properties systems. I will begin with an introduction to abstract interpretation, a theory that makes it possible to automatically synthesize invariant properties on programs. I will then illustrate it with a family of abstract domains based on zonotopes, that are well suited to the analysis of numerical computations. I will in particular demonstrate how they can be adapted to bound the errors due to the use of finite precision to represent real numbers. I will finally end with some examples with the static analyzer Fluctuat.
- Lecture 5 David Pichardie, Inria Rennes & Harvard University, Cambridge, MA, USA. Building verified program analyzers in Coq: a tutorial Nowadays safety critical systems are validated through long and costly test campaigns. Static program analysis is a promising complementary technique that allows to automatically prove the absence of restricted classes of bugs. A significant example is the state-of-the-art Astrée static analyzer for C which has proven some critical safety properties for the primary flight control software of the Airbus A340 fly-by-wire system. Taking note of such a success, the next question is: should we completely remove the test campaign dedicated to the same class of bugs? If we trust the result of the analyzer, of course the answer is yes, but should we trust it? The analyzer itself can be certified by testing, but exhaustivity cannot be achieved. In this tutorial, we will show how mechanized proofs can be used to verify static analyzers themselves. This tutorial will provides a short introduction to the Coq proof assistant and will build a simple verified value analysis inside the CompCert C toolchain.
The school is organized by the labex Digicosme.
- Claude Marché
- Eric Goubault
- Jean Goubault-Larrecq
- Burkhart Wolff