Description
Date depot: 22 juin 2022
Titre: Under-Approximated Program Analysis and Counter-Example Generation by Abstract Interpretation
Directeur de thèse:
Antoine MINE (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Modèles de calcul, preuve, vérification
Resumé: The goal of this PhD proposal is to design, prove correct, implement, and experiment on static program analyses able to discover executions that are formally guaranteed to be erroneous and, dually, infer sufficient conditions for program correctness.
On the theoretical level, the PhD will rely on the theory of abstract interpretation and develop novel abstractions for under-approximations of program states and sufficient preconditions.
On the practical level, the implementation and experimentation will be performed within the MOPSA static analysis platform developed in the APR team at LIP6, Sorbonne Université.
Abstract interpretation is a general theory of the approximation of program semantics, which has been applied to the development of static analyzers to infer automatically program properties and prove program correctness.
The technique is mature enough to handle large and complex programs in real-life languages and has been implemented successfully in effective tools currently used in the industry (such as Astrée and Frama-C).
In order to be efficient, semantic computations are not performed in the precise model of actual program executions (so-called concrete domain) but rather in a simpler, abstract domain, than entail approximations.
The theory and implementation of abstract interpretation is mostly concerned with over-approximating the reachable state set.
This is justified by its main application: formal program validation through a proof of absence of error.
However, in case of an alarm (i.e., an erroneous computation detected in the abstract), we cannot be certain whether the program is indeed incorrect, or the error is only reported due to the over-approximation (so-called false alarm).
To alleviate this problem, backward analyses have been proposed to infer necessary preconditions for the alarms to occur.
Classic backward analyses still compute over-approximations and thus cannot be used to prove the presence of an alarm, leaving the possibility of an inconclusive analysis.
Such proofs would require under-approximated analyses.
The goal of the PhD is to develop new, effective, theoretically and experimentally-proven methods based on abstract interpretation to automatically find sufficient conditions in order for certain program behaviors to occur.
The methods can be applied to one or several of the following problems:
1) Proving that an alarm is a true error and not a false alarm, by inferring a counter-example execution (i.e., a sufficient condition at the entry of the program for the execution to definitely reach the error).
2) Inferring procedure contracts, by inferring assertions that can be inserted at the beginning of a procedure to ensure that its executions will never fail.
3) Evaluating the uncertainty of an analysis by combining the inference of necessary and sufficient conditions, and quantifying the distance between them, possibly iterating analyses in order to improve the precision.
In order to achieve these goals, the work may take inspiration from recent proposals in under-approximating abstract domains, (local) completeness, and incorrectness logic.
The PhD will nevertheless focus on proper abstractions in order to scale to large state spaces with full automation.
The PhD may also explore the combination of over-approximations and under-approximations, as well as forward and backward analyses.
If time permits, the PhD may consider, beyond purely numeric abstractions, data-type abstractions needed for more realistic languages, such as pointers and memory abstractions (lists, etc.).
The intended work will include a theoretical side: developing abstract semantics and proving formally their correctness.
It will also include a practical side: implementing the semantics and validating their benefit experimentally.
The work will be implemented in the MOPSA static analysis platform.
The PhD will experiment the analysis on simple programs in a subset of C or Python, and progressively work towards more realistic programs.
Doctorant.e: Milanese Marco