PhD student
Team : APR
Arrival date : 11/01/2022
    Sorbonne Université - LIP6
    Boîte courrier 169
    Couloir 25-26, Étage 3, Bureau 303
    4 place Jussieu
    75252 PARIS CEDEX 05

Tel: +33 1 44 27 88 16, Marco.Milanese (at)

Supervision : Antoine MINÉ

Under-Approximated Program Analysis and Counter-Example Generation by Abstract Interpretation

The goal of the PhD is to design, prove correct, implement, and experiment on static program analyses to discover executions that are formally guaranteed to be erroneous and, dually, infer sufficient conditions for program correctness.
The PhD will rely on the theory of abstract interpretation and develop novel abstractions for under-approximations of program states. The theory and implementation of abstract interpretation is mostly concerned with over-approximating the reachable state set. In case of an alarm, we cannot be certain whether the program is indeed incorrect, or the error is only reported due to over-approximations (so-called false alarm). Backward analyses have been proposed to infer necessary preconditions for the alarms to occur, but they still compute over-approximations and cannot prove the presence of an alarm, leaving the possibility of an inconclusive analysis. The PhD will develop new, effective, theoretically and experimentally-proven under-approximating backward analysis methods based on abstract interpretation to automatically find sufficient conditions in order for certain program behaviors to occur. The implementation and experimentation will be performed within the MOPSA static analysis platform developed in the APR team at LIP6, Sorbonne Université.