2 Introduction

CELIA is a plug-in of the Frama-C platform which performs static analysis of C programs manipulating (singly linked) lists. More precisely:

• CELIA computes for each line of the program reachable from the main function, an assertion expressing the properties of the lists in the heap of the program.
• CELIA verifies assertions on the program heap given in the C file.

For this, CELIA does a symbolic reachability analysis based on abstract interpretation techniques [Cousot&Cousot'79] and uses special domains and decision procedures for lists.

CELIA is based on several tools released on LGPL licence:

• Frama-C platform for the parsing, typing, and manipulation of C programs,
• Fixpoint library as symbolic fix-point engine on inter-procedural control flow graphs,
• CINV tool for the abstract domains on lists,
• Apron library for the numerical abstract domains.