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