Joint Forces for Memory Safety Checking Revisited

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F20%3A00113978" target="_blank" >RIV/00216224:14330/20:00113978 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/s10009-019-00526-2" target="_blank" >https://doi.org/10.1007/s10009-019-00526-2</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s10009-019-00526-2" target="_blank" >10.1007/s10009-019-00526-2</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Joint Forces for Memory Safety Checking Revisited

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

Joint Forces for Memory Safety Checking Revisited

Popis výsledku anglicky

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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA18-02177S" target="_blank" >GA18-02177S: Abstrakce a jiné techniky v semi-symbolické verifikaci programů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2020

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

International Journal on Software Tools for Technology Transfer (STTT)

ISSN

1433-2779

e-ISSN

1433-2787

Svazek periodika

22

Číslo periodika v rámci svazku

2

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

19

Strana od-do

115-133

Kód UT WoS článku

000521561800003

EID výsledku v databázi Scopus

2-s2.0-85070249446