JONÁŠ, Martin, Kristián KUMOR, Jakub NOVÁK, Jindřich SEDLÁČEK, Marek TRTÍK, Lukáš ZAORAL, Paulína AYAZIOVÁ a 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, s. 406-411. ISBN 978-3-031-57255-5. Dostupné z: https://dx.doi.org/10.1007/978-3-031-57256-2_29.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution
Autoři JONÁŠ, Martin (203 Česká republika, garant, domácí), Kristián KUMOR (703 Slovensko, domácí), Jakub NOVÁK (703 Slovensko, domácí), Jindřich SEDLÁČEK (203 Česká republika, domácí), Marek TRTÍK (203 Česká republika, domácí), Lukáš ZAORAL (203 Česká republika), Paulína AYAZIOVÁ (703 Slovensko, domácí) a Jan STREJČEK (203 Česká republika, domácí).
Vydání 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, od s. 406-411, 6 s. 2024.
Nakladatel Springer
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Německo
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
Organizační jednotka Fakulta informatiky
ISBN 978-3-031-57255-5
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-031-57256-2_29
Klíčová slova anglicky symbolic execution; software verification; Symbiotic
Štítky formal verification, formela-conference, formela-ver, program analysis, program slicing, Symbiotic, verification
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 24. 4. 2024 13:32.
Anotace
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.
Návaznosti
GA23-06506S, projekt VaVNázev: Pokročilá analýza a verifikace pro pokročilý software
Investor: Grantová agentura ČR, Pokročilá analýza a verifikace pro pokročilý software
MUNI/A/1608/2023, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 24
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 24
VytisknoutZobrazeno: 21. 5. 2024 04:53