Heaps and Data Structures: A Challenge for Automated Provers

Sascha Böhme and Michał Moskal

Document: DOI PDF

Abstract: Software verification is one of the most prominent application areas for automated reasoning systems, but their potential improvement is limited by shortage of good benchmarks. Current benchmarks are usually large but shallow, require decision procedures, or have soundness problems. In contrast, we propose a family of benchmarks in first-order logic with equality which is scalable, relatively simple to understand, yet closely resembles difficult verification conditions stemming from real-world C code. Based on this benchmark, we present a detailed comparison of different heap encodings using a number of SMT and ATP systems. Our results led to a performance gain of an order of magnitude for the C code verifier VCC.

Bibtex entry:

@inproceedings{
   author    = {Sascha B{\"o}hme and Micha{\l} Moskal},
   title     = {Heaps and Data Structures: A Challenge for Automated
                Provers},
   booktitle = {Automated Deduction},
   editor    = {Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans},
   series    = {Lecture Notes in Computer Science},
   publisher = {Springer},
   volume    = 6803,
   year      = 2011,
   pages     = {177--191},
}