Handling loops in bounded model checking of C programs via k-induction

Mikhail Y. R. Gadelha, Hussama I. Ismail, Lucas C. Cordeiro

Research output: Contribution to journalArticlepeer-review

174 Downloads (Pure)


The first attempts to apply the k-induction method to software verification are only recent. In this paper, we present a novel proof by induction algorithm, which is built on the top of a symbolic context-bounded model checker and uses an iterative deepening approach to verify, for each step k up to a given maximum, whether a given safety property ϕϕ holds in the program. The proposed k-induction algorithm consists of three different cases, called base case, forward condition, and inductive step. Intuitively, 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 ϕϕ holds in all states reachable within k unwindings; and in the inductive step, we check that whenever ϕϕ holds for k unwindings, it also holds after the next unwinding of the system. The algorithm was implemented in two different ways, a sequential and a parallel one, and the results were compared. Experimental results show that both forms of the algorithm can handle a wide variety of safety properties extracted from standard benchmarks, ranging from reachability to time constraints. And by comparison, the parallel algorithm solves more verification tasks in less time. This paper marks the first application of the k-induction algorithm to a broader range of C programs; in particular, we show that our k-induction method outperforms CPAChecker in terms of correct results, which is a state-of-the-art k-induction-based verification tool for C programs.
Original languageEnglish
Pages (from-to)97-114
JournalInternational Journal on Software Tools for Technology Transfer
Issue number1
Early online date23 Nov 2015
Publication statusPublished - 1 Feb 2017


Dive into the research topics of 'Handling loops in bounded model checking of C programs via k-induction'. Together they form a unique fingerprint.

Cite this