Publication details
Joint Forces for Memory Safety Checking
Authors | |
---|---|
Year of publication | 2018 |
Type | Article in Proceedings |
Conference | Model Checking Software. SPIN 2018 |
MU Faculty or unit | |
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: |