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

Verification of C programs manipulating lists with unbounded data:  

C programs annotated with assertions (pre, post-conditions and loop invariants) in the Singly Linked Lists Logic (SL3), presented at [VMCAI'12] can be verified now using the Celia plugin. The option to be used is -celia-sl3. The SL3 specifications use the ACSL ANSI/ISO C Specification Langage and some specific predicates. See its syntax in ACSL in the sl3.h file.
A sample of verified programs (see also intlist.h and sl3.h):
An extended version of the logic and of the verified examples can be found here!

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