A Verification Toolkit for Numerical Transition Systems (Tool Paper)

This paper reports on an effort to create benchmarks and a toolkit for rigorous verification problems, simplifying tool integration and eliminating ambiguities of complex programming language constructs. We focus on Integer Numerical Transition Systems (INTS), which can be viewed as control-flow graphs whose edges are annotated by Presburger arithmetic formulas. We describe the syntax, semantics, a front-end, and a first release of benchmarks for such transition systems. Furthermore, we present Flata and Eldarica, two new verification tools for INTS. The Flata system is based on precise acceleration of the transition relation, while the Eldarica system is based on predicate abstraction with interpolation-based counterexample-driven refinement. The Eldarica verifier uses the Princess theorem prover as a sound and complete interpolating prover for Presburger arithmetic. Both systems can solve several examples for which previous approaches failed and present a useful baseline for verifying integer programs. Our infrastructure is publicly available; we hope that it will spur further research, benchmarking, competitions, and synergistic communication between verification tools.

Citation

Hossein Hojjat, Filip Konecny, Florent Garnier, Radu Iosif, Viktor Kuncak, and Philipp Ruemmer. A verification toolkit for numerical transition systems (tool paper). In 16th International Symposium on Formal Methods (FM). Springer, 2012.

BibTex Entry

@inproceedings{HojjatETAL12VerificationToolkitNTS,
  author = {Hossein Hojjat and Filip Konecny and Florent Garnier and Radu Iosif and Viktor Kuncak and Philipp Ruemmer},
  title = {A Verification Toolkit for Numerical Transition Systems (Tool Paper)},
  booktitle = {16th International Symposium on Formal Methods (FM)},
  year = 2012,
  publisher = {Springer},
  abstract = {This paper reports on an effort to create benchmarks and a toolkit for
rigorous verification problems, simplifying tool integration and
eliminating ambiguities of complex programming language constructs. We
focus on Integer Numerical Transition Systems (INTS), which can
be viewed as control-flow graphs whose edges are annotated by
Presburger arithmetic formulas. We describe the syntax, semantics, a
front-end, and a first release of benchmarks for such transition
systems. Furthermore, we present Flata and Eldarica,
two new verification tools for INTS. The Flata system is based on
precise acceleration of the transition relation, while the
Eldarica system is based on predicate abstraction with
interpolation-based counterexample-driven refinement. The
Eldarica verifier uses the Princess theorem prover
as a sound and complete interpolating prover for Presburger
arithmetic. Both systems can solve several examples for which previous
approaches failed and present a useful baseline for verifying integer
programs. Our infrastructure is publicly available; we hope that it
will spur further research, benchmarking, competitions, and
synergistic communication between verification tools.}
}