Detail publikace

Verifying LTL Properties of Bytecode with Symbolic Execution

Originální název

Verifying LTL Properties of Bytecode with Symbolic Execution

Anglický název

Verifying LTL Properties of Bytecode with Symbolic Execution

Jazyk

en

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.

Anglický 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.

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",
  annote="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.",
  address="Elsevier Science",
  booktitle="Bytecode 2008",
  chapter="30194",
  edition="NEUVEDEN",
  howpublished="print",
  institution="Elsevier Science",
  journal="ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE",
  year="2008",
  month="april",
  pages="1--14",
  publisher="Elsevier Science",
  type="conference paper"
}