Date: 6 May 2007 07:32:45 -0500

At this Wednesday's ACL2 seminar (usual time and place: 4:00, ACES
3.116):

A Mechanical Analysis of Program Verification Strategies
Sandip Ray

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 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.  In this talk I will provide an outline of
the formalization and the proof, in particular pointing to the importance of
quantification in this work.

This is joint work with Warren A. Hunt Jr., John Matthews, and J Strother
Moore.