@phdthesis{Mon09b,
title = {Analyse statique~: de la th\'eorie \`a la pratique },
author = {Monniaux, David},
month = {jun},
year = {2009},
address = {Grenoble, France},
type = {Habilitation to direct research},
school = {Universit\'e Joseph Fourier},
team = {SYNC,PACSS},
pdf = {http://www-verimag.imag.fr/~monniaux/biblio/Monniaux_HDR.pdf},
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 \soft{Astr\'ee} 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).},
}
