Formula Slicing: Inductive Invariants from Preconditions

TL;DR

This paper introduces formula slicing, a novel method for deriving inductive invariants by weakening preconditions guided by SMT counterexamples, applicable to complex programs and competitive with existing verification techniques.

Contribution

It presents a new formula slicing algorithm that computes the strongest inductive invariants by weakening preconditions using counterexamples, applicable to arbitrary loop structures.

Findings

Effective in deriving invariants for device driver benchmarks

Competitive performance with state-of-the-art verification tools

Applicable to programs with complex loop structures

Abstract

We propose a "formula slicing" method for finding inductive invariants. It is based on the observation that many loops in the program affect only a small part of the memory, and many invariants which were valid before a loop are still valid after. Given a precondition of the loop, obtained from the preceding program fragment, we weaken it until it becomes inductive. The weakening procedure is guided by counterexamples-to-induction given by an SMT solver. Our algorithm applies to programs with arbitrary loop structure, and it computes the strongest invariant in an abstract domain of weakenings of preconditions. We call this algorithm "formula slicing", as it effectively performs "slicing" on formulas derived from symbolic execution. We evaluate our algorithm on the device driver benchmarks from the International Competition on Software Verification (SV-COMP), and we show that it is competitive with the state-of-the-art verification techniques.