Michał Moskal

Heaps and Data Structures: A Challenge for Automated Provers

Sascha Böhme, Michał Moskal

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.


  • The paper [PDF]
  • Updated experiment results (with proper options for E) [PDF]
  • The Boogie files, and generation scripts [TAR.BZ2]
  • Benchmarks in TPTP format [TAR.BZ2]
  • Benchmarks in SMT (v1) format [TAR.BZ2]

Back to Michal's homepage

 > People > Michal Moskal