Detail publikace

Verifying LTL Properties of Bytecode with Symbolic Execution

BRAIONE, P. DENARO, G. PEZZE, M. KŘENA, B.

Originální název

Verifying LTL Properties of Bytecode with Symbolic Execution

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

Symbolic execution, code-based model checking of software.

Autoři

BRAIONE, P.; DENARO, G.; PEZZE, M.; KŘENA, B.

Rok RIV

2008

Vydáno

5. 4. 2008

Nakladatel

Elsevier Science

Místo

Budapest

ISSN

1571-0661

Periodikum

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE

Stát

Spojené státy americké

Strany od

1

Strany do

14

Strany počet

14

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"
}