Joint Forces for Memory Safety Checking

• 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
• 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