2LS: Heap Analysis and Memory Safety (Competition Contribution)
This work addresses memory safety and program verification challenges for developers and researchers in software analysis, but it is incremental as it builds on existing CPROVER infrastructure.
The paper tackles the problem of verifying and refuting assertions and termination in sequential C programs, particularly for dynamic data structures, by extending the 2LS framework to handle combined shape and content reasoning and memory safety instrumentation.
2LS is a framework for analysis of sequential C programs that can verify and refute program assertions and termination. The 2LS framework is built upon the CPROVER infrastructure and implements template-based synthesis techniques, e.g. to find invariants and ranking functions, and incremental loop unwinding techniques to find counterexamples and k-induction proofs. The main improvements in this year's version are the ability of 2LS to analyse programs requiring combined reasoning about shape and content of dynamic data structures, and an instrumentation for memory safety properties.