Joint Forces for Memory Safety Checking

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři	CHALUPA Marek STREJČEK Jan VITOVSKÁ Martina
Rok publikování	2018
Druh	Článek ve sborníku
Konference	Model Checking Software. SPIN 2018
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Doi	http://dx.doi.org/10.1007/978-3-319-94111-0_7
Klíčová slova	program analysis; program verification; memory safety
Popis	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.
Související projekty:	Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII. Abstrakce a jiné techniky v semi-symbolické verifikaci programů Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18