A Mechanical Analysis of Program Verification Strategies

We analyze three proof strategies commonly used in deductive verification of deterministic sequential programs formalized with operational semantics. The strategies are (i)  stepwise invariants , (ii)  clock functions , and (iii)  inductive assertions . We show how to formalize the strategies in the...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2008-05, Vol.40 (4), p.245-269
Main Authors: Ray, Sandip, Hunt, Warren A., Matthews, John, Moore, J. Strother
Format: Article
Language:English
Subjects:
Artificial Intelligence
Computer Science
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Studies
Symbolic and Algebraic Manipulation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We analyze three proof strategies commonly used in deductive verification of deterministic sequential programs formalized with operational semantics. The strategies are (i)  stepwise invariants , (ii)  clock functions , and (iii)  inductive assertions . We show how to formalize the strategies in the logic of the ACL2 theorem prover. Based on our formalization, we prove that each strategy is both sound and complete . The completeness result implies that given any proof of correctness of a sequential program one can derive a proof in each of the above strategies. The soundness and completeness theorems have been mechanically checked with ACL2.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-008-9098-1