CHALUPA, Marek, Vincent MIHALKOVIČ, Anna ŘECHTÁČKOVÁ, Lukáš ZAORAL a Jan STREJČEK. Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding. In Dana Fisman and Grigore Rosu. Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II. Cham (Švýcarsko): Springer, Cham. s. 462-467. ISBN 978-3-030-99526-3. doi:10.1007/978-3-030-99527-0_32. 2022.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding
Autoři CHALUPA, Marek (203 Česká republika, domácí), Vincent MIHALKOVIČ (703 Slovensko, domácí), Anna ŘECHTÁČKOVÁ (203 Česká republika, domácí), Lukáš ZAORAL (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí).
Vydání Cham (Švýcarsko), Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II, od s. 462-467, 6 s. 2022.
Nakladatel Springer, Cham
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Švýcarsko
Utajení není předmětem státního či obchodního tajemství
Forma vydání elektronická verze "online"
WWW URL
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/22:00125696
Organizační jednotka Fakulta informatiky
ISBN 978-3-030-99526-3
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-030-99527-0_32
UT WoS 000782398900032
Klíčová slova anglicky Symbiotic;BSELF;SV-COMP;program analysis;verification
Štítky formela-ver, program analysis, Symbiotic, verification
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 28. 3. 2023 12:49.
Anotace
The development of Symbiotic 9 focused mainly on two components. One is the symbolic executor Slowbeast, which newly supports backward symbolic execution including its extension called loop folding. This technique can infer inductive invariants from backward symbolic execution states. Thanks to these invariants, Symbiotic 9 is able to produce non-trivial correctness witnesses, which is a feature that is missing in previous versions of Symbiotic. We have also extended forward symbolic execution in Slowbeast with a basic support for parallel programs. The second component with significant improvements is the instrumentation module. In particular, we have extended the static analysis of accesses to arrays with features designed for programs that manipulate C strings. Symbiotic 9 is the Overall winner of SV-COMP 2022. Moreover, it won also the categories MemSafety and SoftwareSystems, and placed third in FalsificationOverall.
Návaznosti
GA19-24397S, projekt VaVNázev: Automaty v rozhodovacích procedurách a verifikaci (Akronym: AUTODEV)
Investor: Grantová agentura ČR, Automata for Decision Procedures and Verification
MUNI/A/1145/2021, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace XI. (Akronym: SV-FI MAV XI.)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace XI.
MUNI/A/1230/2021, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 22 (Akronym: SKOMU)
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 22
VytisknoutZobrazeno: 28. 3. 2024 14:40