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.

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

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"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Organizační jednotka

Fakulta informatiky

ISBN

978-3-031-57255-5

ISSN

DOI

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

UT WoS

001284187100029

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ěněno: 18. 10. 2024 16:56, prof. RNDr. Jan Strejček, Ph.D.

Anotace

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.

Návaznosti

GA23-06506S, projekt VaV
Ná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/1592/2023, interní kód MU
Název: Modelování, analýza a verifikace (2024)
Investor: Masarykova univerzita, Modelování, analýza a verifikace (2024)
MUNI/A/1608/2023, interní kód MU
Ná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
Zobrazeno: 15. 11. 2024 17:36