Publication details

Joint Forces for Memory Safety Checking

Investor logo
Authors

CHALUPA Marek STREJČEK Jan VITOVSKÁ Martina

Year of publication 2018
Type Article in Proceedings
Conference Model Checking Software. SPIN 2018
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-94111-0_7
Keywords program analysis; program verification; memory safety
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info