Theory Refinement [experimental]

The right choice of a domain-specific constraint language enables automated verifiers to scale up to large problems.
Satisfiability modulo theories (SMT) solvers implement efficient decision procedures for the constraint languages, but fall short on built-in support for choosing a constraint language which is expressive enough to model a given program.
The theory refinement approach is our experimental feature on HiFrog that enables abstraction refinement directly guided by programs, and build on the core SMT concept of theories.
The approach has been implemented in the OpenSMT2 SMT solver to leverage bit-precise verification of programs with non-linear arithmetic.
The implementation uses an augmented version of the theory of uninterpreted functions and is capable of directly injecting non-clausal refinements to the inherent Boolean structure of SMT.
Our prototype implementation is available below as a virtual machine containing both the binaries and the benchmark set.  The prototype is competitive with the widely used propositional flattening approach and is several orders of magnitudes faster on some of our benchmark instances.
 
Downloads:
  • A virtual machine containing the runnable system; if password needed, it is “hifrog”
  • Preliminary evaluation reports are available here. (mostly from SV-COMP16 and SV-COMP15).
  • How to compile HiFrog for theory Refinement? Please follow the instruction here.
  • Benchmarks