Supervision : Antoine MINÉ

Incremental Static Analysis for Program Verification

Frama-C is a code analysis platform for C programs which provides several analyzers as plug-ins. Frama-C can ensure that a C program satisfies its formal specification by relying on several techniques including abstract interpretation, weakest preconditions calculus, and runtime assertion checking. Inside Frama-C, Eva is a plugin dedicated to the automatic inference of properties about C programs such as finding all the possible values of variables or inferring arithmetic relations between variables. The primary goal of this analysis is to prove the absence of runtime execution errors (e.g. arithmetic overflows, invalid memory accesses, other C undefined behaviors, ...). It is also used for code auditing and as a support for other analyses. It performs an abstract interpretation of the program which has the advantage of being completely automatic (no user interaction is needed during the analysis) and scalable. In an industrial framework it is often required to run these analyses incrementally. There are two (overlapping) use cases of an incremental analysis. 1. During the development of a safety critical software, analyses can be run to detect flaws early or to ensure that the software will be easily validated with such analyses as soon as the validation phase starts. The continuous validation of the software will require numerous analyses to be run between each patch, and the cumulated computation cost might hinder the methodology. In this context, it is also possible to analyze the semantic differences induced by each patch. 2. A certification process taking place after the initial development and usually by a distinct team can rely on a successful analysis. While this would require only one analysis, past experience shows that such an analysis would have to be finely tuned to achieve this goal. In practice, this tuning is done incrementally by adjusting the analysis parameters at each iteration until the tool succeeds in proving the absence of runtime errors. The cost of this process is one order of magnitude higher than the cost of one analysis and might be prohibitive. It is crucial in both scenarios that subsequent analyses cost considerably less than the first analysis. However, the reuse of previous results in abstract interpretation is still an open subject. The proposed solutions will be implemented in Eva, but should be general enough for being easily adapted to other tools such as Mopsa and E-ACSL.

2024 Publications