2LS for Program Analysis

TL;DR

2LS is a verification tool for C programs that uses second-order logic formulas and incremental SAT solving to efficiently verify assertions, memory safety, and termination properties, with a flexible framework for invariant synthesis.

Contribution

It introduces a modular approach combining unfolding and template-based invariant synthesis within a fast incremental bounded model checking framework.

Findings

Fast incremental bounded model checking algorithm

Flexible framework for invariant inference experiments

Effective verification of assertions and safety properties

Abstract

2LS ("tools") is a verification tool for C programs, built upon the CPROVER framework. It allows one to verify user-specified assertions, memory safety properties (e.g. buffer overflows), numerical overflows, division by zero, memory leaks, and termination properties. The analysis is performed by translating the verification task into a second-order logic formula over bitvector, array, and floating-point arithmetic theories. The formula is solved by a modular combination of algorithms involving unfolding and template-based invariant synthesis with the help of incremental SAT solving. Advantages of 2LS include its very fast incremental bounded model checking algorithm and its flexible framework for experimenting with novel analysis and abstraction ideas for invariant inference. Drawbacks are its lack of support for certain program features (e.g. multi-threading).