The research, funded by the ASOPT project, will focus on newer methods for static analysis and invariant generation by abstract interpretation, including, but not exclusively :
  • Use of SMT-solving.

  • Reduction to optimization or quantifier elimination problems.

  • Alternative iteration schemes (e.g. policy iteration).

The post-doc will be supervised by Dr David Monniaux, research associate at CNRS.


VERIMAG (director: Nicolas Halbwachs) is a joint laboratory between the French national center for scientific research (CNRS) and the University of Grenoble. It is specialized in methods for designing and analyzing safe computing systems, including programming language design (e.g. Lustre) and verification techniques (both abstract interpretation and model-checking have roots in Grenoble).

VERIMAG is located in Gières, a suburb of Grenoble, a city of approximately 430000 inhabitants in the French Alps. Grenoble is a first-grade academic center, with numerous laboratories, including the international organizations ESRF (European synchrotron radiation facility) and the ILL (Institut Laue-Langevin). In addition, Grenoble is surrounded by mountains and skiing resorts, and is an internationally renowned center for paragliding.

About the position:

The post-doc will be employed as a temporary contract worker by CNRS, for one year.