Result Details
Automatic Verification of Integer Array Programs
IOSIF, R.; KONEČNÝ, F.; VOJNAR, T.; HABERMEHL, P.; BOZGA, M. Automatic Verification of Integer Array Programs. TR-2009-2, Grenoble: VERIMAG, 2009. 49 p.
Type
report
Language
English
Authors
Radu Iosif
Konečný Filip, Ing., Ph.D., DITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Habermehl Peter
Bozga Marius
Konečný Filip, Ing., Ph.D., DITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Habermehl Peter
Bozga Marius
Abstract
This report is the full version of an CAV'09 paper.We provide a verification technique for a class of programs working on\emph{integer
arrays} of finite, but not a priori bounded length. We use the logic of integer arrays \textbf{SIL} \cite{lpar08} to
specify pre- and post-conditions of programs and their parts. Effects of non-looping parts of code are computed
syntactically on the level of \textbf{SIL}. Loop pre-conditions derived during the computation in \textbf{SIL} are
converted into counter automata (CA). Loops are automatically translated---purely on the syntactical level---to
transducers. Pre-condition CA and transducers are composed, and the composition over-approximated by flat automata with
difference bound constraints, which are next converted back into \textbf{SIL} formulae, thus inferring post-conditions
of the loops. Finally, validity of post-conditions specified by the user in \textbf{SIL} may be checked as entailment is
decidable for \textbf{SIL}.
arrays} of finite, but not a priori bounded length. We use the logic of integer arrays \textbf{SIL} \cite{lpar08} to
specify pre- and post-conditions of programs and their parts. Effects of non-looping parts of code are computed
syntactically on the level of \textbf{SIL}. Loop pre-conditions derived during the computation in \textbf{SIL} are
converted into counter automata (CA). Loops are automatically translated---purely on the syntactical level---to
transducers. Pre-condition CA and transducers are composed, and the composition over-approximated by flat automata with
difference bound constraints, which are next converted back into \textbf{SIL} formulae, thus inferring post-conditions
of the loops. Finally, validity of post-conditions specified by the user in \textbf{SIL} may be checked as entailment is
decidable for \textbf{SIL}.
Keywords
formal verification, arrays, automata, mathematical logic
URL
Published
2009
Pages
49
Publisher
VERIMAG
Place
TR-2009-2, Grenoble
BibTeX
@misc{BUT192689,
author="Iosif {Radu} and Filip {Konečný} and Tomáš {Vojnar} and Peter {Habermehl} and Marius {Bozga}",
title="Automatic Verification of Integer Array Programs",
year="2009",
pages="49",
publisher="VERIMAG",
address="TR-2009-2, Grenoble",
url="http://www-verimag.imag.fr/TR/TR-2009-2.pdf"
}
Projects
Advanced Formal Approaches in the Design and Verification of Computer-Based Systems, GACR, Standardní projekty, GA102/07/0322, start: 2007-01-01, end: 2009-12-31, completed
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
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
Research groups
Departments