The First DigiCosme Spring School takes place in April 22-26, 2013.

This page provides various material for the lectures: slides, lecture notes, exercises and such; including updates to what is distributed with the USB memory stick.

Jean-Christophe Filliâtre
LRI, CNRS & University Paris-Sud, Orsay, France
Deductive Program Verification with Why3
Burkhart Wolff
LRI, CNRS & University Paris-Sud, Orsay, France
Model-based Testing with Isabelle-HOL-TestGen
Cédric Fournet
Microsoft Research, Cambridge, UK
Modular Code-Based Cryptographic Verification by Typing
Sylvie Putot
CEA-List & Ecole Polytechnique, Palaiseau, France
Static analysis of numerical programs and systems
David Pichardie
Inria Rennes & Harvard University, Cambridge, MA, USA
Building verified program analyzers in Coq: a tutorial