Detail publikace

Verifying LTL Properties of Bytecode with Symbolic Execution

BRAIONE Pietro, DENARO Giovanni, PEZZE Mauro a KŘENA Bohuslav. Verifying LTL Properties of Bytecode with Symbolic Execution. In: Bytecode 2008. Budapest: Elsevier Science, 2008, s. 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
angličtina
Autoři
Braione Pietro (DISCo, LTA)
Denaro Giovanni (DISCo, LTA)
Pezze Mauro (DISCo, LTA)
Křena Bohuslav, Ing., Ph.D. (UITS FIT VUT)
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
Konference
Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation, Budapest, HU
Vydavatel
Elsevier Science
Místo
Budapest, HU
BibTeX 
@INPROCEEDINGS{FITPUB8686,
   author = "Pietro Braione and Giovanni Denaro and Mauro Pezze and Bohuslav K\v{r}ena",
   title = "Verifying LTL Properties of Bytecode with Symbolic Execution",
   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 = "https://www.fit.vut.cz/research/publication/8686"
}
Nahoru