Přístupnostní navigace
E-application
Search Search Close
Publication detail
BRAIONE, P. DENARO, G. PEZZE, M. KŘENA, B.
Original Title
Verifying LTL Properties of Bytecode with Symbolic Execution
Type
article in a collection out of WoS and Scopus
Language
English
Original 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.
Keywords
Symbolic execution, code-based model checking of software.
Authors
BRAIONE, P.; DENARO, G.; PEZZE, M.; KŘENA, B.
RIV year
2008
Released
5. 4. 2008
Publisher
Elsevier Science
Location
Budapest
ISBN
1571-0661
Periodical
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE
State
United States of America
Pages from
1
Pages to
14
Pages count
BibTex
@inproceedings{BUT30194, author="Pietro {Braione} and Giovanni {Denaro} and Mauro {Pezze} and Bohuslav {Křena}", title="Verifying LTL Properties of Bytecode with Symbolic Execution", booktitle="Bytecode 2008", year="2008", journal="ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE", pages="1--14", publisher="Elsevier Science", address="Budapest", issn="1571-0661" }