CTL
19 June 2009 - 10h15
Static analysis: from theory to practice (HDR)
by David Monniaux from CNRS / VERIMAG
Abstract: Software operating critical systems (aircraft, nuclear power plants) should not fail — whereas most computerised systems of daily life (personal computer, ticket vending machines, cell phone) fail from time to time. This is not a simple engineering problem: it is known, since the works of Turing and Cook, that proving that programs work correctly is intrinsically hard.
In order to solve this problem, one needs methods that are, at the same time, efficient (moderate costs in time and memory), safe (all possible failures should be found), and precise (few warnings about nonexistent failures). In order to reach a satisfactory compromise between these goals, one can research fields as diverse as formal logic, numerical analysis or classical algorithmics.
From 2002 to 2007 I participated in the development of the Astrée static analyser. This suggested to me a number of side projects, both theoretical and practical (use of formal proof techniques, analysis of numerical filters...). More recently, I became interested in modular analysis of numerical property and in the applications to program analysis of constraint solving techniques (semidefinite programming, SAT and SAT modulo theory).
HDR, Jury composé de :
- Roberto Giacobazzi, professeur à l'Université de Vérone, rapporteur
- Éric Goubault, chercheur au CEA et professeur à l'École polytechnique, rapporteur
- Andreas Podelski, professeur à l'Université Albert-Ludwigs de Freiburg, rapporteur
- Gilles Dowek, professeur à l'École polytechnique
- Roland Groz, professeur à Grenoble-INP
- Helmut Seidl, professeur à l'Université technique de Munich
