Publication detail

A Verification Toolkit for Numerical Transition Systems

KONEČNÝ, F. HOJJAT, H. IOSIF, R. KUNCAK, V. RUMMER, P. GARNIER, F.

Original Title

A Verification Toolkit for Numerical Transition Systems

English Title

A Verification Toolkit for Numerical Transition Systems

Type

journal article - other

Language

en

Original Abstract

This paper reports a toolkit and a benchmark suite for rigorous verification of Integer Numerical Transition Systems (INTS), which can be viewed as control-flow graphs whose edges are annotated by Presburger arithmetic formulas. We present FLATA and ELDARICA, two 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.

English abstract

This paper reports a toolkit and a benchmark suite for rigorous verification of Integer Numerical Transition Systems (INTS), which can be viewed as control-flow graphs whose edges are annotated by Presburger arithmetic formulas. We present FLATA and ELDARICA, two 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.

Keywords

integer programs, numerical transition systems, verification, acceleration, predicate abstraction

RIV year

2012

Released

12.05.2012

Publisher

Springer Verlag

Location

NEUVEDEN

Pages from

247

Pages to

251

Pages count

4

Documents

BibTex


@article{BUT96983,
  author="Filip {Konečný} and Hossein {Hojjat} and Iosif {Radu} and Viktor {Kuncak} and Philipp {Rummer} and Florent {Garnier}",
  title="A Verification Toolkit for Numerical Transition Systems",
  annote="This paper reports a toolkit and a benchmark suite for rigorous verification of
Integer Numerical Transition Systems (INTS), which can be viewed as control-flow
graphs whose edges are annotated by Presburger arithmetic formulas. We present
FLATA and ELDARICA, two 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.",
  address="Springer Verlag",
  booktitle="Proceedings of FM'12",
  chapter="96983",
  edition="NEUVEDEN",
  howpublished="print",
  institution="Springer Verlag",
  number="7436",
  volume="2012",
  year="2012",
  month="may",
  pages="247--251",
  publisher="Springer Verlag",
  type="journal article - other"
}