Detail publikace

Symbiotic 8: Beyond Symbolic Execution

CHALUPA Marek, JAŠEK Tomáš, NOVÁK Jakub, ŘECHTÁČKOVÁ Anna, STREJČEK Jan a ŠOKOVÁ Veronika. Symbiotic 8: Beyond Symbolic Execution. In: Proceedings of TACAS 2021 (2). Lecture Notes in Computer Science, roč. 12652. Cham: Springer International Publishing, 2021, s. 453-457. ISBN 978-3-030-72012-4.
Název česky
Symbiotic 8: Kromě symbolické exekuce (příspěvek do soutěže)
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Chalupa Marek, RNDr. (FI MUNI)
Jašek Tomáš, Bc. (FI MUNI)
Novák Jakub, Bc. (FI MUNI)
Řechtáčková Anna, Bc. (FI MUNI)
Strejček Jan, prof. RNDr., Ph.D. (FI MUNI)
Šoková Veronika, Ing. (UITS FIT VUT)
Abstrakt

Symbiotic 8 rozšiřuje tradiční kombinaci statických analýz, instrumentace, prořezávání programu a symbolického provádění o jednu podstatnou novinku, a to spojení symbolického provádění s k-indukcí. Touto technikou lze prokázat správnost programů s potenciálně neomezenými cykli, které nelze vykonat klasickým symbolickým prováděním. Symbiotic 8 přináší také několik dalších vylepšení. Zejména jsme upravili naši verzi symbolického exekutora Klee, tak, aby podporoval porovnávání symbolických ukazatelů. Dále jsme vyladili nástroj tvarové analýzy Predator (integrovaný již v Symbioticu 7), aby fungoval lépe na LLVM IR. Vyvinuli jsme také odlehčenou analýzu vztahů mezi proměnnými, která může prokázat absenci přístupů za hranice polí.

Rok
2021
Strany
453-457
Sborník
Proceedings of TACAS 2021 (2)
Řada
Lecture Notes in Computer Science
Svazek
12652
Konference
European Joint Conferences on Theory and Practice of Software -- ETAPS'21 (TACAS'21), Lucemburk, LU
ISBN
978-3-030-72012-4
Vydavatel
Springer International Publishing
Místo
Cham, CH
DOI
EID Scopus
BibTeX
@INPROCEEDINGS{FITPUB12444,
   author = "Marek Chalupa and Tom\'{a}\v{s} Ja\v{s}ek and Jakub Nov\'{a}k and Anna \v{R}echt\'{a}\v{c}kov\'{a} and Jan Strej\v{c}ek and Veronika \v{S}okov\'{a}",
   title = "Symbiotic 8: Beyond Symbolic Execution",
   pages = "453--457",
   booktitle = "Proceedings of TACAS 2021 (2)",
   series = "Lecture Notes in Computer Science",
   volume = 12652,
   year = 2021,
   location = "Cham, CH",
   publisher = "Springer International Publishing",
   ISBN = "978-3-030-72012-4",
   doi = "10.1007/978-3-030-72013-1\_31",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/12444"
}
Nahoru