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):
- List reverse: intlist-fold-reverse.c
- List initialization: copy data and add some value intlist-map2-addV_eq.c
- List initialization: set some value in all elements intlist-map-initV.c
- List initialization: set values to the Fibonacci sequence intlist-map-initFibo.c
- List initialization: set values to (01)* sequence intlist-map-initMod2.c
- List initialization: set values to first natural numbers intlist-map-initSeq.c
- Find a value in a sorted list intlist-sorted-find.c
- Insert a value in a sorted list intlist-sorted-insert.c
- Concatenates two sorted lists with disjoint intervals of values intlist-sorted-concat.c
An extended version of the logic and of the verified examples can be found here!