Symbiotic 10: Lazy Memory Initialization and Compact Symbolic
Execution

D 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:

URL

Impact factor

Impact factor: 0.402 in 2005

Organization unit

Faculty of Informatics

ISBN

978-3-031-57255-5

ISSN

DOI

http://dx.doi.org/10.1007/978-3-031-57256-2_29

UT WoS

001284187100029

Keywords in English

symbolic execution; software verification; Symbiotic

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

Name: Pokročilá analýza a verifikace pro pokročilý software

Investor: Czech Science Foundation, Advanced Analysis and Verification for Advanced Software

MUNI/A/1592/2023, interní kód MU

Name: Modelování, analýza a verifikace (2024)

Investor: Masaryk University, Modeling, analysis, and verification (2024)

MUNI/A/1608/2023, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 24

Investor: Masaryk University

Citovat

JONÁŠ, Martin, Kristián KUMOR, Jakub NOVÁK, Jindřich SEDLÁČEK, Marek TRTÍK, Lukáš ZAORAL, Paulína AYAZIOVÁ and Jan STREJČEK. Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution. Online. In Bernd Finkbeiner and Laura Kovács. 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. Cham (Švýcarsko): Springer, 2024, p. 406-411. ISBN 978-3-031-57255-5. Available from: https://dx.doi.org/10.1007/978-3-031-57256-2_29.

@inproceedings{2396645,
   author = {Jonáš, Martin and Kumor, Kristián and Novák, Jakub and Sedláček, Jindřich and Trtík, Marek and Zaoral, Lukáš and Ayaziová, Paulína and Strejček, Jan},
   address = {Cham (Švýcarsko)},
   booktitle = {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},
   doi = {http://dx.doi.org/10.1007/978-3-031-57256-2_29},
   editor = {Bernd Finkbeiner and Laura Kovács},
   keywords = {symbolic execution; software verification; Symbiotic},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham (Švýcarsko)},
   isbn = {978-3-031-57255-5},
   pages = {406-411},
   publisher = {Springer},
   title = {Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution},
   url = {https://link.springer.com/book/10.1007/978-3-031-57256-2_29},
   year = {2024}
}

TY  - JOUR
ID  - 2396645
AU  - Jonáš, Martin - Kumor, Kristián - Novák, Jakub - Sedláček, Jindřich - Trtík, Marek - Zaoral, Lukáš - Ayaziová, Paulína - Strejček, Jan
PY  - 2024
TI  - Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution
PB  - Springer
CY  - Cham (Švýcarsko)
SN  - 9783031572555
KW  - symbolic execution
KW  - software verification
KW  - Symbiotic
UR  - https://link.springer.com/book/10.1007/978-3-031-57256-2_29
N2  - 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.
ER  -

JONÁŠ, Martin, Kristián KUMOR, Jakub NOVÁK, Jindřich SEDLÁČEK, Marek TRTÍK, Lukáš ZAORAL, Paulína AYAZIOVÁ and Jan STREJČEK. Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution. Online. In Bernd Finkbeiner and Laura Kovács. \textit{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}. Cham (Švýcarsko): Springer, 2024, p.~406-411. ISBN~978-3-031-57255-5. Available from: https://dx.doi.org/10.1007/978-3-031-57256-2\_{}29.

Detailed Information on Publication Record