CHALUPA, Marek, Jan STREJČEK a Martina VITOVSKÁ. Joint Forces for Memory Safety Checking Revisited. International Journal on Software Tools for Technology Transfer (STTT). Springer, 2020, roč. 22, č. 2, s. 115-133. ISSN 1433-2779. Dostupné z: https://dx.doi.org/10.1007/s10009-019-00526-2.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Joint Forces for Memory Safety Checking Revisited
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í International Journal on Software Tools for Technology Transfer (STTT), Springer, 2020, 1433-2779.
Další údaje
Originální jazyk angličtina
Typ výsledku Článek v odborném periodiku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
WWW URL
Impakt faktor Impact factor: 0.739
Kód RIV RIV/00216224:14330/20:00113978
Organizační jednotka Fakulta informatiky
Doi http://dx.doi.org/10.1007/s10009-019-00526-2
UT WoS 000521561800003
Klíčová slova anglicky memory safety; instrumentation; program slicing; symbolic execution; Symbiotic
Štítky bug-detection, formal verification, formela-journal, program analysis, program slicing, 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. 2021 07:54.
Anotace
We present an improved version of the memory safety verification approach implemented in Symbiotic 5, the winner of the MemSafety category at the Competition on Software Verification (SV-COMP) 2018. The approach can verify programs for standard errors in memory usage like invalid pointer dereference or memory leaking. It is based on instrumentation, static pointer analysis extended to consider memory deallocations, static program slicing, and symbolic execution. The improved version brings higher precision of the extended pointer analysis and further optimizations in instrumentation. It is implemented in the current version of Symbiotic, which contains also some improvements in program slicing and symbolic execution. We explain the approach in theory, describe implementation of selected components, and provide experimental results showing the impact 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/1050/2019, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX (Akronym: SV-FI MAV IX)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 24. 4. 2024 17:30