Scaling Bounded Model Checking By Transforming Programs With Arrays

TL;DR

This paper introduces a transformation technique that converts array-manipulating programs into array-free, loop-free versions, enabling more efficient bounded model checking of array properties with reduced resource consumption.

Contribution

The authors present a novel program transformation that enables bounded model checkers to verify array properties more efficiently by eliminating loops and arrays, with formal guarantees of soundness and precision.

Findings

Reduces resource requirements for model checking large array programs

Transforms array-manipulating programs into array-free, loop-free versions

Demonstrates effectiveness on industry and benchmark code

Abstract

Bounded Model Checking is one the most successful techniques for finding bugs in program. However, model checkers are resource hungry and are often unable to verify programs with loops iterating over large arrays.We present a transformation that enables bounded model checkers to verify a certain class of array properties. Our technique transforms an array-manipulating (ANSI-C) program to an array-free and loop-free (ANSI-C) program thereby reducing the resource requirements of a model checker significantly. Model checking of the transformed program using an off-the-shelf bounded model checker simulates the loop iterations efficiently. Thus, our transformed program is a sound abstraction of the original program and is also precise in a large number of cases - we formally characterize the class of programs for which it is guaranteed to be precise. We demonstrate the applicability and usefulness of our technique on both industry code as well as academic benchmarks.