Model Checking C Programs with Loops via k-Induction and Invariants

TL;DR

This paper introduces a new k-induction based algorithm for model checking C programs with loops, leveraging invariants and polyhedral constraints to improve verification effectiveness.

Contribution

It combines k-induction with invariant inference using polyhedral constraints, enhancing the ability to verify safety properties in programs with loops.

Findings

Polyhedral invariants improve verification success rate.

The combined k-induction and invariants approach handles more safety properties.

Implementation with polyhedral invariants outperforms without invariants.

Abstract

We present a novel proof by induction algorithm, which combines k-induction with invariants to model check C programs with bounded and unbounded loops. The k-induction algorithm consists of three cases: in the base case, we aim to find a counterexample with up to k loop unwindings; in the forward condition, we check whether loops have been fully unrolled and that the safety property P holds in all states reachable within k unwindings; and in the inductive step, we check that whenever P holds for k unwindings, it also holds after the next unwinding of the system. For each step of the k-induction algorithm, we infer invariants using affine constraints (i.e., polyhedral) to specify pre- and post-conditions. The algorithm was implemented in two different ways, with and without invariants using polyhedral, and the results were compared. Experimental results show that both forms can handle a wide variety of safety properties; however, the k-induction algorithm adopting polyhedral solves more verification tasks, which demonstrate an improvement of the induction algorithm effectiveness.