CINV
Verification of Programs with Dynamic Lists

• Introduction
• Examples
• Download
• Credits
• References

CINV is a tool for abstract reachability analysis of programs manipulating dynamic (singly linked) lists. It implements a generic abstract domain HS for reasoning about dynamic lists with unbounded data which includes an abstraction on the shape of the heap and which is parametrized by some abstract domain on finite sequences of data (a data words abstract domain, DW-domain for short). The DW-domain is intended to abstract the sequences of data in the lists by capturing relevant aspects such as their sizes, the sums or the multisets of their elements, or some class of constraints on their data at different (linearly ordered or successive) positions.

CINV provides (for the moment) two classes of DW-domains:

• The first class, LSUM, represents constraints relating data, length, and sums of data of list segments. In this class, several abstract domains can be obtained by varying the underlying numerical domain used (interval, octagons, polyhedra) and the kind (product or mixed) of relation allowed between the lengths and the sums of segments lists.
• The second class, UCONS, relates data and lengths of lists segments through first-order formulas. These formulas have a special form: forall y. (P => U), where y is a vector of variables on the positions in the word, P is a constraint on the positions (seen as integers) associated with the y's, and U is a constraint on the data values at these positions, and possibly also on the positions when data are of numerical type.

We have applied CINV to a large class of programs manipulating lists. In particular, we have carried out the analysis of several sorting algorithms, of lists traversals with computation of complex arithmetical relations, etc. These programs are available on the distributed package (see Download, directory samples/src). A detailed presentation of results is given in the following documentation:

• HTML version,
• PDF version.

CINV is a free software under LGPL license. You can download the CINV tool via HTTP.

For installing CINV you need:

• autoconf/automake.
• An ANSI C compiler (only gcc with ansi option has been tested).
• INTERPROC distribution which includes APRON and asks for downloading other tools or libraries (Ocaml, Camlidl, PPL).

Participants to the CINV project:

• Ahmed Bouajjani
• Cezara Dragoi.
• Constantin Enea
• Mihaela Sighireanu

[BDERS10] A. Bouajjani, C. Dragoi, C. Enea, A. Rezine, and M. Sighireanu. Invariant Synthesis for Programs Manipulating Lists with Unbounded Data Long version of a paper submitted for publication. January 2010.

Last updated: Tue Jan 12 2010