Symbiotic 9: String Analysis and Backward Symbolic Execution
with Loop Folding

D 2022

Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding

CHALUPA, Marek, Vincent MIHALKOVIČ, Anna ŘECHTÁČKOVÁ, Lukáš ZAORAL, Jan STREJČEK et. al.

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

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"

Odkazy

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

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ěněno: 28. 3. 2023 12:49, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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 VaV

Ná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 MU

Ná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 MU

Ná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

Citovat

CHALUPA, Marek, Vincent MIHALKOVIČ, Anna ŘECHTÁČKOVÁ, Lukáš ZAORAL a Jan STREJČEK. Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding. Online. 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, 2022, s. 462-467. ISBN 978-3-030-99526-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-99527-0_32.

@inproceedings{1848419,
   author = {Chalupa, Marek and Mihalkovič, Vincent and Řechtáčková, Anna and Zaoral, Lukáš and Strejček, Jan},
   address = {Cham (Švýcarsko)},
   booktitle = {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},
   doi = {http://dx.doi.org/10.1007/978-3-030-99527-0_32},
   editor = {Dana Fisman and Grigore Rosu},
   keywords = {Symbiotic;BSELF;SV-COMP;program analysis;verification},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham (Švýcarsko)},
   isbn = {978-3-030-99526-3},
   pages = {462-467},
   publisher = {Springer, Cham},
   title = {Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding},
   url = {https://link.springer.com/chapter/10.1007/978-3-030-99527-0_32},
   year = {2022}
}

TY  - JOUR
ID  - 1848419
AU  - Chalupa, Marek - Mihalkovič, Vincent - Řechtáčková, Anna - Zaoral, Lukáš - Strejček, Jan
PY  - 2022
TI  - Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding
PB  - Springer, Cham
CY  - Cham (Švýcarsko)
SN  - 9783030995263
KW  - Symbiotic;BSELF;SV-COMP;program analysis;verification
UR  - https://link.springer.com/chapter/10.1007/978-3-030-99527-0_32
N2  - 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.
ER  -

CHALUPA, Marek, Vincent MIHALKOVIČ, Anna ŘECHTÁČKOVÁ, Lukáš ZAORAL a Jan STREJČEK. Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding. Online. In Dana Fisman and Grigore Rosu. \textit{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, 2022, s.~462-467. ISBN~978-3-030-99526-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-99527-0\_{}32.

Podrobný výpis o publikaci