Files and binaries for experimental results of TACAS 2018 paper "A Verified Implementation of the Bounded List Container"

This dataset contains files and binaries as described in the TACAS 2018 paper "A Verified Implementation of the Bounded List Container".

The formal verification of the container libraries provided by programming languages is of importance for their intensive use in safety- and security- critical applications. This dataset and the accompanying paper provide an implementation mimicking the bounded doubly linked list container, a GNAT implementation of the doubly linked lists container in the standard library of Ada 2012. This implementation was formally verified using an auto-active verification approach, supported by the prototype tool VeriFast. A distribution of this tool is provided in the /verifast-v17.06-79-g6cad329 directory.

The implementation is provided as a C library, with code annotated for formal verification with VeriFast (cfdlli.c and cfdlli.h). Also provided are additional logic definitions that extend the logic libraries of VeriFast to deal with models implemented here (vflist.gh, vfseq.gh and vfmap.gh).

Additional scripts to reproduce the statistics presented in section 4 of the accompanying paper are also provided (count_annot.sh and stats.sh).

Further details on reproducing the experiments presented can be found in README.txt.