Faculty of Information Technology, BUT

Publication Details

Verifying LTL Properties of Bytecode with Symbolic Execution

BRAIONE Pietro, DENARO Giovanni, PEZZE Mauro and KŘENA Bohuslav. Verifying LTL Properties of Bytecode with Symbolic Execution. In: Bytecode 2008. Budapest: Elsevier Science, 2008, pp. 1-14. ISSN 1571-0661.
Czech title
Využití symbolického provádění bytekódu pro ověřování LTL vlastností
Type
conference paper
Language
english
Authors
Braione Pietro (DISCo, LTA)
Denaro Giovanni (DISCo, LTA)
Pezze Mauro (DISCo, LTA)
Křena Bohuslav, Ing., Ph.D. (DITS FIT BUT)
Keywords
Symbolic execution, code-based model checking of software.
Abstract

Bytecode languages are at a very desirable degree of abstraction for performing formal analysis of programs, but at the same time pose new challenges when compared with traditional languages. This paper proposes a methodology for bytecode analysis which harmonizes two well-known formal verification techniques, model checking and symbolic execution. Model checking is a property-guided exploration of the system state space until the property is proved or disproved, producing in the latter case a counterexample execution trace. Symbolic execution emulates program execution by replacing concrete variable values with symbolic ones, so that the symbolic execution along a path represents the potentially infinite numeric executions that may occur along that path. We propose an approach where symbolic execution is used for building a possibly partial model of the program state space, and on-the-fly model checking is exploited for verifying temporal properties on it. The synergy of the two techniques yields considerable potential advantages: symbolic execution allows for modeling the state space of infinite-state software systems, limits the state explosion, and fosters modular verification; model checking provides fully automated verification of reachability properties of a program. To assess these potential advantages, we report our preliminary experience with the analysis of a safety-critical software system.

Published
2008
Pages
1-14
Journal
Electronic Notes in Theoretical Computer Science, ISSN 1571-0661
Proceedings
Bytecode 2008
Conference
Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation, Budapest, HU
Publisher
Elsevier Science
Place
Budapest, HU
BibTeX
@INPROCEEDINGS{FITPUB8686,
   author = "Pietro Braione and Giovanni Denaro and Mauro Pezze and Bohuslav K\v{r}ena",
   title = "Verifying LTL Properties of Bytecode with Symbolic Execution",
   pages = "1--14",
   booktitle = "Bytecode 2008",
   journal = "Electronic Notes in Theoretical Computer Science",
   year = 2008,
   location = "Budapest, HU",
   publisher = "Elsevier Science",
   ISSN = "1571-0661",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8686"
}
Back to top