1/1
Prototype and benchmarks for "Invariant Synthesis for Incomplete Verification Engines"
dataset
posted on 2018-04-12, 10:25 authored by Daniel Neider, Pranav Garg, P. Madhusudan, Shambwaditya Saha, Daejun ParkThis dataset contains the prototype and benchmarks described in the paper "Invariant Synthesis for Incomplete Verification Engines". The software and data comprise a general, learning-based invariant synthesis framework that learns invariants using non-provability information provided by verification engines.
This artifact has been designed and tested on the TACAS 2018 Artifact Evaluation VM: Hartmanns, Arnd; Wendler, Philipp (2018). figshare. https://doi.org/10.6084/m9.figshare.5896615. However, it is likely to run on any 64-bit Linux environment.
This artifact contains precompiled binaries (located in ./binaries) as well as sources (located in ./sources). To reproduce the experimental results reported in the paper, we highly recommend using the precompiled binaries. However, for users to compile the sources themselves, please follow the instructions at the end of this document.
Our tool is built on top of the Boogie program verifier and the Z3 theorem prover. These tools are interfaced via various scripts as described below.
This artifact contains two sets of benchmarks: heap-manipulating programs (located in ./heaps) and programs whose specifications involve universal quantification (located in ./quantifier). All benchmarks are provided as .bpl programs (Boogie verification language). In the case of heap-manipulating programs, this archive also contains the original C programs from which the .bpl programs have been generated using VCDryad.
To perform the natural proofs transformation and generation of Boogie programs yourself, please follow the instructions in the README.txt file. The quantifier benchmarks were hand-crafted.
The ./sources subdirectory contains scripts and documentation for both the intermediate verification language Boogie and the SMT solver Z3.
The binaries to compile both Boogie and node.js are located in ./binaries. The individual shell scripts (.sh) at the highest level directory can be used to run individual experiments.
Backgound
In the related TACAS 2018 publication we propose a framework for synthesizing inductive invariants for incomplete verification engines, which soundly reduce logical problems in undecidable theories to decidable theories. Our framework is based on the counter-example guided inductive synthesis principle (CEGIS) and allows verification engines to communicate non-provability information to guide invariant synthesis. We show precisely how the verification engine can compute such non-provability information and how to build effective learning algorithms when invariants are expressed as Boolean combinations of a fixed set of predicates. Moreover, we evaluate our framework in two verification settings, one in which verification engines need to handle quantified formulas and one in which verification engines have to reason about heap properties expressed in an expressive but undecidable separation logic.
