Software verification using k-induction
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 sep...
| Príomhchruthaitheoirí: | , , , |
|---|---|
| Rannpháirtithe: | |
| Formáid: | Conference item |
| Foilsithe / Cruthaithe: |
Springer
2011
|
| _version_ | 1826291635528400896 |
|---|---|
| author | Donaldson, A Haller, L Kroening, D Rummer, P |
| author2 | Yahav, E |
| author_facet | Yahav, E Donaldson, A Haller, L Kroening, D Rummer, P |
| author_sort | Donaldson, A |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T03:02:22Z |
| format | Conference item |
| id | oxford-uuid:b161b5e2-f533-4330-bad2-5d146a2f1802 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T03:02:22Z |
| publishDate | 2011 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:b161b5e2-f533-4330-bad2-5d146a2f18022022-03-27T04:03:40ZSoftware verification using k-inductionConference itemhttp://purl.org/coar/resource_type/c_5794uuid:b161b5e2-f533-4330-bad2-5d146a2f1802Symplectic Elements at OxfordSpringer2011Donaldson, AHaller, LKroening, DRummer, PYahav, EWe 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. |
| spellingShingle | Donaldson, A Haller, L Kroening, D Rummer, P Software verification using k-induction |
| title | Software verification using k-induction |
| title_full | Software verification using k-induction |
| title_fullStr | Software verification using k-induction |
| title_full_unstemmed | Software verification using k-induction |
| title_short | Software verification using k-induction |
| title_sort | software verification using k induction |
| work_keys_str_mv | AT donaldsona softwareverificationusingkinduction AT hallerl softwareverificationusingkinduction AT kroeningd softwareverificationusingkinduction AT rummerp softwareverificationusingkinduction |