Proving Safety with Trace Automata and Bounded Model Checking

TL;DR

This paper introduces a method using trace automata to eliminate redundant execution traces in loop under-approximation, enabling more efficient safety verification with bounded model checking without false positives.

Contribution

The paper proposes a novel trace automata-based technique to reduce redundant traces after loop acceleration, improving the effectiveness of bounded model checking for safety proofs.

Findings

Reduces program diameter, aiding safety proofs.

No false positives introduced by the transformation.

Experimental results demonstrate applicability and efficiency.

Abstract

Loop under-approximation is a technique that enriches C programs with additional branches that represent the effect of a (limited) range of loop iterations. While this technique can speed up the detection of bugs significantly, it introduces redundant execution traces which may complicate the verification of the program. This holds particularly true for verification tools based on Bounded Model Checking, which incorporate simplistic heuristics to determine whether all feasible iterations of a loop have been considered. We present a technique that uses \emph{trace automata} to eliminate redundant executions after performing loop acceleration. The method reduces the diameter of the program under analysis, which is in certain cases sufficient to allow a safety proof using Bounded Model Checking. Our transformation is precise---it does not introduce false positives, nor does it mask any errors. We have implemented the analysis as a source-to-source transformation, and present experimental results showing the applicability of the technique.