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.
- Read the publications.
- See samples of programs analyzed.
- See samples of programs verified.
- See the documentation for CELIA.
- Download CELIA (with CINV).
- See also some extensions.
Participants to the CELIA project: