Publication Details
Verifying LTL Properties of Bytecode with Symbolic Execution
Denaro Giovanni (DISCo, LTA)
Pezze Mauro (DISCo, LTA)
Křena Bohuslav, Ing., Ph.D. (DITS FIT BUT)
Symbolic execution, code-based model checking of software.
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.
@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" }