Result Details

A Verification Toolkit for Numerical Transition Systems

KONEČNÝ, F.; HOJJAT, H.; IOSIF, R.; KUNCAK, V.; RUMMER, P.; GARNIER, F. A Verification Toolkit for Numerical Transition Systems. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7436, p. 247-251. ISSN: 0302-9743.
Type
journal article
Language
English
Authors
Konečný Filip, Ing., Ph.D., DITS (FIT)
Hojjat Hossein
Radu Iosif
Kuncak Viktor
Rummer Philipp
Garnier Florent
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

Published
2012
Pages
247–251
Journal
Lecture Notes in Computer Science, vol. 2012, no. 7436, ISSN 0302-9743
Book
Proceedings of FM'12
Publisher
Springer Verlag
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",
  journal="Lecture Notes in Computer Science",
  year="2012",
  volume="2012",
  number="7436",
  pages="247--251",
  issn="0302-9743"
}
Projects
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, start: 2011-01-01, end: 2015-12-31, completed
Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit, MŠMT, COST, OC10009, start: 2010-01-01, end: 2012-12-31, running
Mathematical and Engineering Approaches to Developing Reliable and Secure Concurrent and Distributed Computer Systems, GACR, Doktorské granty, GD102/09/H042, start: 2009-01-30, end: 2012-12-31, completed
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, start: 2007-01-01, end: 2013-12-31, running
Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness, GACR, Standardní projekty, GAP103/10/0306, start: 2010-01-01, end: 2013-12-31, running
Verifikace a optimalizace počítačových systémů, BUT, Vnitřní projekty VUT, FIT-S-12-1, start: 2012-01-01, end: 2014-12-31, completed
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top