Model Checking C Programs with Loops via k-Induction and 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.
Keywords
Cite
@article{arxiv.1502.02327,
title = {Model Checking C Programs with Loops via k-Induction and Invariants},
author = {Herbert Rocha and Hussama Ismail and Lucas Cordeiro and Raimundo Barreto},
journal= {arXiv preprint arXiv:1502.02327},
year = {2015}
}