CHALUPA, Marek, Jan STREJČEK a Martina VITOVSKÁ. Joint Forces for Memory Safety Checking. In María-del-Mar Gallardo and Pedro Merino. Model Checking Software. SPIN 2018. Cham, Švýcarsko: Springer. s. 115-132. ISBN 978-3-319-94110-3. doi:10.1007/978-3-319-94111-0_7. 2018.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Joint Forces for Memory Safety Checking
Autoři CHALUPA, Marek (203 Česká republika, domácí), Jan STREJČEK (203 Česká republika, garant, domácí) a Martina VITOVSKÁ (203 Česká republika, domácí).
Vydání Cham, Švýcarsko, Model Checking Software. SPIN 2018, od s. 115-132, 18 s. 2018.
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í tištěná verze "print"
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/18:00101043
Organizační jednotka Fakulta informatiky
ISBN 978-3-319-94110-3
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-94111-0_7
UT WoS 000455352500007
Klíčová slova anglicky program analysis; program verification; memory safety
Štítky firank_B, formela-conference, program analysis, Symbiotic
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 29. 4. 2019 15:39.
Anotace
The paper describes a successful approach to checking computer programs for standard memory handling errors like invalid pointer dereference or memory leaking. The approach is based on four well-known techniques, namely pointer analysis, instrumentation, static program slicing, and symbolic execution. We present a particular very efficient combination of these techniques, which has been implemented in the tool Symbiotic and won by a large margin the MemSafety category of SV-COMP 2018. We explain the approach and provide a detailed analysis of effects of particular components.
Návaznosti
GA18-02177S, projekt VaVNázev: Abstrakce a jiné techniky v semi-symbolické verifikaci programů
Investor: Grantová agentura ČR, Abstrakce a jiné techniky v semi-symbolické verifikaci programů
MUNI/A/0854/2017, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII.
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/1038/2017, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 28. 3. 2024 12:40