J 2020

Joint Forces for Memory Safety Checking Revisited

CHALUPA, Marek, Jan STREJČEK a Martina VITOVSKÁ

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

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í

Odkazy

Impakt faktor

Impact factor: 0.739

Kód RIV

RIV/00216224:14330/20:00113978

Organizační jednotka

Fakulta informatiky

DOI

UT WoS

000521561800003

Klíčová slova anglicky

memory safety; instrumentation; program slicing; symbolic execution; Symbiotic

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 29. 4. 2021 07:54, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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 VaV
Ná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 MU
Ná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