Publication detail

Verifying LTL Properties of Bytecode with Symbolic Execution

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

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