Unbounded Software Model Checking with Incremental SAT-Solving

TL;DR

This paper introduces LLUMC, a novel unbounded software model checking method using incremental SAT-solving with DimSpec formulas, capable of analyzing large and infinite loops efficiently and supporting parallel SAT-solving for runtime optimization.

Contribution

It presents a new encoding of C program errors into DimSpec formulas and integrates incremental SAT-solving and IC3 algorithms for unbounded model checking.

Findings

Expands bounded model checkers to handle large and infinite loops.

Maintains feasible time performance in complex program analysis.

Enables runtime optimizations through parallel SAT-solving.

Abstract

This paper describes a novel unbounded software model checking approach to find errors in programs written in the C language based on incremental SAT-solving. Instead of using the traditional assumption based API to incremental SAT solvers we use the DimSpec format that is used in SAT based automated planning. A DimSpec formula consists of four CNF formulas representing the initial, goal and intermediate states and the relations between each pair of neighboring states of a transition system. We present a new tool called LLUMC which encodes the presence of certain errors in a C program into a DimSpec formula, which can be solved by either an incremental SAT-based DimSpec solver or the IC3 algorithm for invariant checking. We evaluate the approach in the context of SAT-based model checking for both the incremental SAT-solving and the IC3 algorithm. We show that our encoding expands the functionality of bounded model checkers by also covering large and infinite loops, while still maintaining a feasible time performance. Furthermore, we demonstrate that our approach offers the opportunity to generate runtime-optimizations by utilizing parallel SAT-solving.