Journal article

KONEČNÝ Filip, HOJJAT Hossein, IOSIF Radu, KUNCAK Viktor, RUMMER Philipp and GARNIER Florent. A Verification Toolkit for Numerical Transition Systems. Lecture Notes in Computer Science. 2012, vol. 2012, no. 7436, pp. 247-251. ISSN 0302-9743.
Publication language:english
Original title:A Verification Toolkit for Numerical Transition Systems
Title (cs):Toolkit pro verifikaci numerických přechodivých systémů
Book:Proceedings of FM'12
Journal:Lecture Notes in Computer Science, Vol. 2012, No. 7436, DE
Publisher:Springer Verlag
integer programs, numerical transition systems, verification, acceleration, predicate abstraction
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.
   author = {Filip Kone{\v{c}}n{\'{y}} and Hossein Hojjat and Radu Iosif
	and Viktor Kuncak and Philipp Rummer and Florent Garnier},
   title = {A Verification Toolkit for Numerical Transition Systems},
   pages = {247--251},
   booktitle = {Proceedings of FM'12},
   journal = {Lecture Notes in Computer Science},
   volume = {2012},
   number = {7436},
   year = {2012},
   publisher = {Springer Verlag},
   ISSN = {0302-9743},
   language = {english},
   url = {}

Your IPv4 address:
Switch to IPv6 connection

DNSSEC [dnssec]