Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F22%3A00125696" target="_blank" >RIV/00216224:14330/22:00125696 - isvavai.cz</a>
Result on the web
<a href="https://link.springer.com/chapter/10.1007/978-3-030-99527-0_32" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-030-99527-0_32</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-030-99527-0_32" target="_blank" >10.1007/978-3-030-99527-0_32</a>
Alternative languages
Result language
angličtina
Original language name
Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA19-24397S" target="_blank" >GA19-24397S: Automata for Decision Procedures and Verification</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2022
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
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
ISBN
9783030995263
ISSN
0302-9743
e-ISSN
—
Number of pages
6
Pages from-to
462-467
Publisher name
Springer, Cham
Place of publication
Cham (Švýcarsko)
Event location
Munich, Germany
Event date
Jan 1, 2022
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000782398900032