Plugin for Static Analysis and Verification of C Programs with Dynamic Lists

CELIA architecture

CELIA is a tool for the static analysis and verification of C programs manipulating dynamic lists.
The static analyser computes for each control point of a C program the assertions which are true (i.e., invariant) at this control point. These asssertions express properties about the shape of the lists, their size, the relations between the data (or the sum, or the multiset of data) in list cells. The analysis is inter-procedural, i.e., the assertions computed relate the procedure local heap on entry to the corresponding local heap on exit of the procedure. The results of the analysis can provide insights about equivalence of procedures on lists or null pointer dereferencing.
The verifier checks specifications written in a logic combining Separation Logic and a first order logic over sequences of integers.

CELIA is a plug-in of the Frama-C platform and it uses the heap abstract domains provided by the CINV library, the numerical domains provided by APRON, and the fixpoint computation engine FIXPOINT.

Participants to the CELIA project:

See also:    APRON    CINV    Frama-C    FIXPOINT    ANR Project Veridyc