A Mechanical Analysis of Program Verification Strategies |
| |
Authors: | Sandip Ray,Warren A. Hunt Suffix" >Jr.,John Matthews,J. Strother Moore |
| |
Affiliation: | (1) Department of Computer Sciences, The Unversity of Texas at Austin, Austin, TX 78712, USA;(2) Galois Inc., Beaverton, OR 97005, USA |
| |
Abstract: | 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. |
| |
Keywords: | Inductive assertions Invariants Partial correctness Theorem proving Total correctness |
本文献已被 SpringerLink 等数据库收录! |
|