Detail publikace
Symbiotic 8: Beyond Symbolic Execution
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)
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í.
@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" }