Detailed Information on Publication Record
2024
Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution
JONÁŠ, Martin, Kristián KUMOR, Jakub NOVÁK, Jindřich SEDLÁČEK, Marek TRTÍK et. al.Basic information
Original name
Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution
Authors
JONÁŠ, Martin (203 Czech Republic, guarantor, belonging to the institution), Kristián KUMOR (703 Slovakia, belonging to the institution), Jakub NOVÁK (703 Slovakia, belonging to the institution), Jindřich SEDLÁČEK (203 Czech Republic, belonging to the institution), Marek TRTÍK (203 Czech Republic, belonging to the institution), Lukáš ZAORAL (203 Czech Republic), Paulína AYAZIOVÁ (703 Slovakia, belonging to the institution) and Jan STREJČEK (203 Czech Republic, belonging to the institution)
Edition
Cham (Švýcarsko), Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III, p. 406-411, 6 pp. 2024
Publisher
Springer
Other information
Language
English
Type of outcome
Stať ve sborníku
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
Germany
Confidentiality degree
není předmětem státního či obchodního tajemství
Publication form
electronic version available online
References:
Impact factor
Impact factor: 0.402 in 2005
Organization unit
Faculty of Informatics
ISBN
978-3-031-57255-5
ISSN
UT WoS
001284187100029
Keywords in English
symbolic execution; software verification; Symbiotic
Tags
Tags
International impact, Reviewed
Změněno: 18/10/2024 16:56, prof. RNDr. Jan Strejček, Ph.D.
Abstract
V originále
Symbiotic 10 brings four substantial improvements. First, we extended our clone of Klee called JetKlee with lazy memory initialization. With this extension, JetKlee can symbolically execute a function without knowing its context. In SV-COMP, we use it to handle extern variables. Second, we have implemented the technique called compact symbolic execution to Slowbeast. Third, we have implemented a non-trivial may-happen-in-parallel analysis, which improves slicing of parallel programs. Finally, we have implemented support for violation witnesses in the new witness format 2.0.
Links
GA23-06506S, research and development project |
| ||
MUNI/A/1592/2023, interní kód MU |
| ||
MUNI/A/1608/2023, interní kód MU |
|