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é.

2023-2024 Publications

• 2024
  • R. Monat, M. Milanese, F. Parolini, J. Boillot, A. Ouadjaout, A. Miné : “Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution)”, Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2024, vol. 14572, Lecture Notes in Computer Science, Luxembourg City, Luxembourg, pp. 387-392, (Springer Nature Switzerland) (2024)
• 2023
  • M. Milanese, A. Miné : “Generation of Violation Witnesses by Under-Approximating Abstract Interpretation”, (2023)