Verification of Programs with Dynamic Lists





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:

For all these domains, CINV implements the APRON interface of abstract domains and uses the fixpoint computation engines of INTERPROC.


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:


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

For installing CINV you need:


Participants to the CINV project:


[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