Keywords: Program verification, abstract interpretation, certified static analysis

Scientific context and subject description

Static analysis tools are used to prove that safety-critical software systems do not exhibit undesirable behaviours. Examples of such tools include PolySpace Verifier and Astrée. Such tools are themselves very complex, and industrial users are rightly concerned that they may themselves contain bugs. One thus would like to prove them correct, in the same way that there now exists CompCert, a C compiler that has been mathematically proved to compile programs faithfully.

Convex polyhedra have long been used for static analysis (since 1978!) and thus it would be interesting to have an efficient way to certify the results of polyhedral abstract operations (e.g. a fast certifying implementation of the simplex algorithm), that is, have formal proofs of correctness of the results of these operations. In addition, some symbolic propagation technique (conversion to SSA form, or linearization) are often used and themselves need certification. Ideally, one would like to have a certified or certifying version of the APRON library.

Furthermore, in the last years, a number of new static analysis techniques (policy iteration, path focusing, reductions to mathematical programming...) have been explored. The student could explore which parts of these algorithms are to be proved correct to ensure soundness, and whether proofs of correctness may be replaced by generation of witnesses to be verified by a certified checker.

Project context

This work will be a part of the national project VERASCO (formal VERification of Static Analysers and COmpilers) funded by ANR (Agence Nationale de la Recherche), in cooperation with other academic and industrial partners: INRIA Paris-Rocquencourt (Abstraction and Gallium projects), INRIA / IRISA Rennes (Celtique project), INRIA Saclay-Île de France (Proval project) and Airbus Operations SAS, a leading manufacturer of jet airplanes.

Project VERASCO is coordinated by Xavier Leroy at the inter-laboratory level, and by David Monniaux locally at VERIMAG.

Laboratory

The student will be enrolled at the VERIMAG laboratory.

VERIMAG is a joint laboratory of CNRS (French national center for scientific research) and Grenoble University (Université Joseph Fourier). It is located in Gières, a near suburb of Grenoble, a major scientific and technological center in France.

Advisors

The PhD will be advised or co-advised by one or two of the researchers involved in the project at VERIMAG:

Practical details

This is a three years PhD studentship funded by ANR. The position is expected to start in October-December 2011, though later dates are possible.

The student will be enrolled in the PhD program at Université Joseph Fourier. In addition to research work, the program includes graduate classes. Tuition costs are a few hundred euros per year, and are to be paid by the student.

The student will be an employee of CNRS. In addition to the salary, the position comes with competitive unemployment, health, retirement and other benefits. This contract is not renewable, but short-term extensions may be available depending on the availability of funding.

In addition to research work, the student may also teach at the university, with extra pay.

Since all scientific staff speak English, there is no need for the applicant to speak French, though this may help in daily life (e.g. dealing with banks and the like) and may be required for the optional teaching appointment. It is possible to get French classes.

How to apply

Applicants must have a Master degree (or equivalent 4 or 5-year degree) in Computer Science, Applied Mathematics or other relevant field. Good programming skills are required. Experience with Formal Verification, SAT (satisfiability solving), SMT (Satisfiability modulo theory), abstract interpretation, convex programming and/or proof assistants (e.g. Coq) is a plus.

Applicants should email a CV and the contact information of one reference to David.Monniaux AT imag.fr, Michael.Perin AT imag.fr and Pierre.Corbineau AT imag.fr. There is no need to contact the university services at this point.