2LS: Heap Analysis and Memory Safety (Competition Contribution)

TL;DR

2LS is an advanced framework for analyzing C programs that verifies assertions, termination, and memory safety, using synthesis and incremental techniques, with improvements in handling dynamic data structures and memory safety properties.

Contribution

The paper introduces new capabilities in 2LS to analyze programs involving complex shape and content reasoning of dynamic data structures and memory safety properties.

Findings

Enhanced analysis of programs with dynamic data structures.

Ability to verify memory safety properties.

Improved counterexample and proof generation techniques.

Abstract

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.