Paper Info
Title
Software verification using k-induction
Abstract
We present combined-case k-induction, a novel technique for verifying software programs. This technique draws on the strengths of the classical inductive-invariant method and a recent application of k-induction to program verification. In previous work, correctness of programs was established by separately proving a base case and inductive step. We present a new k-induction rule that takes an unstructured, reducible control flow graph (CFG), a natural loop occurring in the CFG, and a positive integer k, and constructs a single CFG in which the given loop is eliminated via an unwinding proportional to k. Recursively applying the proof rule eventually yields a loop-free CFG, which can be checked using SAT-/SMT-based techniques. We state soundness of the rule, and investigate its theoretical properties. We then present two implementations of our technique: K-INDUCTOR, a verifier for C programs built on top of the CBMC model checker, and K-BOOGIE, an extension of the Boogie tool. Our experiments, using a large set of benchmarks, demonstrate that our k-induction technique frequently allows program verification to succeed using significantly weaker loop invariants than are required with the standard inductive invariant approach.
Year
DOI
Venue
2011
10.1007/978-3-642-23702-7_26
SAS
Keywords
Field
DocType
novel technique,k-induction technique,single cfg,proof rule,smt-based technique,software verification,combined-case k-induction,loop-free cfg,new k-induction rule,program verification,natural loop,computer science
Programming language,Model checking,Control flow graph,Computer science,Correctness,Algorithm,Theoretical computer science,Software,Loop invariant,Soundness,Recursion,Software verification
Conference
Volume
ISSN
Citations 
6887
0302-9743
22
PageRank 
References 
Authors
0.80
13
4
Name
Order
Citations
PageRank
Alastair F. Donaldson166152.35
Leopold Haller21276.93
Daniel Kroening33084187.60
Philipp Rümmer465543.87