This page contains supplementary material for the following paper

This paper is an improved, extended version of a paper the authors have presented at the International Joint Conference on Automated Reasoning (IJCAR 2020) and also at the 35th Italian Conference on Computational Logic 2020 (CILC 2020).

Besides detailed proofs and examples, the main, new contribution consists in addressing the problem of the completeness of the transformations. In our previous version, we proved only a soundness property, ensuring that if the transformed clauses are satisfiable, then so are the original clauses. In this paper, we identify some sufficient conditions, related to the functionality of the difference predicates introduced by the transformation algorithm R, which guarantee the converse of soundness, that is, if the transformed clauses are unsatisfiable, then so are the original ones. We have also extended our implementation and our benchmark, and we have shown that our sufficient conditions can indeed be checked in many interesting, non trivial examples. The page for the supplementary material for the conference version of the paper can be accessed here.

Benchmark suite and experiments

Our benchmark suite consists of 251 verification problems over inductively defined data structures, such as lists, queues, heaps, and trees. 168 of these problems consider properties that do hold (valid properties) and the remaining 83 consider properties that do not hold (invalid properties). The 168 problems have been adapted from the benchmark suite considered by Reynolds and Kuncak, and originate from benchmarks used by various theorem provers, such as CLAM, HipSpec, IsaPlanner, and Leon. Invalid properties have been obtained from valid properties by either negating the valid properties or introducing suitable bugs in the predicates on which the properties depend.

You can browse Alternatively, you can download an archive with all the problems.

A spreadsheet file with more detailed experimental results is available, too.

ADTRem tool

Instructions for running the tool on Linux 64bit.