DigiCosme SpringSchool 2013
The first DigiCosme Spring School took place from April 22th to 26th, 2013, at the Supélec campus of Gif which is located on the Plateau de Saclay, France (around 25 km in the south of Paris).
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, modelbased 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:0010:30  Lecture 2  Lecture 3  Lecture 4  Lecture 5  
10:3011:00  break  break  break  break  
11:0012:30  Lecture 2  Lecture 3  Lecture 4  Lecture 5  
12:3014:30  lunch  lunch  lunch  lunch  lunch 
14:3016:00  Lecture 1  Lecture 3  Lecture 4  Lecture 5  
16:0016:30  break  break  break  break  
16:3018:00  Lecture 1  Lecture 3  Lecture 4  Lecture 5 

JeanChristophe Filliâtre, LRI, CNRS & University ParisSud, Orsay, France. Deductive Program Verification with Why3Lecture 1 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 firstorder logic, and a technology to verify programs using interactive and automated theorem provers (Coq, AltErgo, 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.).

Burkhart Wolff, LRI, CNRS & University ParisSud, Orsay, France. Modelbased Testing with IsabelleHOLTestGenLecture 2 Many testing techniques vitally depend on symbolic computation and constraintsolving techniques. Their limits therefore represent limits for testing as a whole. The HOLTestGen system is designed as plugin into the stateoftheart theorem proving environment Isabelle/HOL. Thus, powerful modeling languages as well as powerful automated and interactive proof methods for constraint resolution are available. HOLTestGen has been applied in unit, sequence, and reactive sequence blackbox 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 casestudies.

Cédric Fournet, Microsoft Research, Cambridge, UK. Verification of protocols and of their implementationsLecture 3 
Sylvie Putot, CEAList & Ecole Polytechnique, Palaiseau, France. Static analysis of numerical programs and systemsLecture 4 Proving the software reliability of safetycritical 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.

David Pichardie, Inria Rennes & Harvard University, Cambridge, MA, USA. Building verified program analyzers in Coq: a tutorialLecture 5 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 stateoftheart Astrée static analyzer for C which has proven some critical safety properties for the primary flight control software of the Airbus A340 flybywire 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.
Organization, Contact
The school is organized by the labex Digicosme.Program committee:
 Claude Marché
 Eric Goubault
 Jean GoubaultLarrecq
 Burkhart Wolff