Joint Forces for Memory Safety Checking

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, 2018, s. 115-132. ISBN 978-3-319-94110-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-94111-0_7.

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

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

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

---

Anotace

V originále

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 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/0854/2017, interní kód MU	Ná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 MU	Ná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