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í
Proceedings:Bytecode 2008
Conference:Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation
Place:Budapest, HU
Journal:Electronic Notes in Theoretical Computer Science, US
Publisher:Elsevier Science
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.

   author = {Pietro Braione and Giovanni Denaro and Mauro Pezze
	and Bohuslav K{\v{r}}ena},
   title = {Verifying LTL Properties of Bytecode with Symbolic
   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 = {}

Your IPv4 address:
Switch to https