Detail publikace

Verifying LTL Properties of Bytecode with Symbolic Execution

BRAIONE, P.; DENARO, G.; PEZZE, M.; KŘENA, B. Verifying LTL Properties of Bytecode with Symbolic Execution. Bytecode 2008. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE. Budapest: Elsevier Science, 2008. p. 1-14. ISSN: 1571-0661.
Název česky
Využití symbolického provádění bytekódu pro ověřování LTL vlastností
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Braione Pietro
Denaro Giovanni
Pezze Mauro, prof.
Křena Bohuslav, Ing., Ph.D. (UITS)
Klíčová slova

Symbolic execution, code-based model checking of software.

Abstrakt

Úroveň abstrakce bytecode jazyků je velice vhodná pro formální analýzu programů v nich vytvořených. Na druhou stranu je třeba řešit nové problémy, které se zde objevují na rozdíl od klasických programovacích jazyků. V tomto článku je navržena metodologie pro analýzu bytecode, která využívá dvě známé metody formální verifikace: model checking a symbolické provádění.

Rok
2008
Strany
1–14
Časopis
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, ISSN 1571-0661
Sborník
Bytecode 2008
Vydavatel
Elsevier Science
Místo
Budapest
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"
}
Nahoru