Conference paper

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.
Publication language:english
Original title:Verifying LTL Properties of Bytecode with Symbolic Execution
Title (cs):Využití symbolického provádění bytekódu pro ověřování LTL vlastností
Pages:1-14
Proceedings:Bytecode 2008
Conference:Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation
Place:Budapest, HU
Year:2008
Journal:Electronic Notes in Theoretical Computer Science, US
ISSN:1571-0661
Publisher:Elsevier Science
Keywords
Symbolic execution, code-based model checking of software.
Annotation

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.

BibTeX:
@INPROCEEDINGS{
   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 = {http://www.fit.vutbr.cz/research/view_pub.php?id=8686}
}

Your IPv4 address: 54.162.218.214
Switch to IPv6 connection

DNSSEC [dnssec]