- Verification of C programs:
Extension of the verifier to allow a more expressive logic SLAD over lists and arrays with unbounded data.
The list of verified programs (see also the old list of programs and compare the size of formulas):- Slad definition: slad.h
- Creates a list from an input list with all data increased by some data parameter: intlist-copyaddV.c
- Initializes data in a list with consecutive values starting from some data parameter: intlist-map-initSeq.c
- Set values to the Fibonacci sequence intlist-map-initFibo.c
- Set as strictly sorted lists: add an element setlist-add.c
- Set as strictly sorted lists: test of membership setlist-contains.c
- Set as strictly sorted lists: difference of two sets setlist-difference.c
- Set as strictly sorted lists: intersection of two sets setlist-intersect.c
- Set as strictly sorted lists: union of two sets setlist-union.c
- Set as strictly sorted lists: client program setlist-client.c
- SVCOMP example: set values to (01)* sequence svcomp-list-prop.c
- Arrays and lists: creates a list from an array array-tolist.c
- Arrays and lists: creates an array from a list intlist-toarray.c
- Accurate entailment checking for logic on lists and arrays:
The decision procedure for entailment checking of SLAD formulas is available as a tool taking as input entailment problems in the SMTLIB 2 format.
Some examples of entailments belonging to the AUFLIA which has been checked using our decision procedure:- From the verification of intlist-fold-reverse.c:
- From the verification of intlist-map2-addV_eq.c:
- From the verification of intlist-map-initV.c:
- From the verification of intlist-map-initFibo.c:
- From the verification of intlist-map-initSeq.c:
- From the verification of intlist-map-initMod2.c:
- From the verification of intlist-sorted-find.c:
- From the verification of intlist-sorted-insert.c: