Detail publikačního výsledku

A Verification Toolkit for Numerical Transition Systems

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

Originální název

A Verification Toolkit for Numerical Transition Systems

Anglický název

A Verification Toolkit for Numerical Transition Systems

Druh

Článek recenzovaný mimo WoS a Scopus

Originální abstrakt

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.

Anglický abstrakt

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.

Klíčová slova

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

Klíčová slova v angličtině

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

Autoři

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

Rok RIV

2013

Vydáno

12.05.2012

Nakladatel

Springer Verlag

Kniha

Proceedings of FM'12

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Svazek

2012

Číslo

7436

Stát

Spolková republika Německo

Strany od

247

Strany do

251

Strany počet

4

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"
}