Date: Mon, 8 Dec 2003 11:27:22 -0600 (CST)
From: Sandip Ray
To: acl2-mtg@lists.cc.utexas.edu
Subject: This week in ACL2
Content-Type: TEXT/PLAIN; charset=US-ASCII
Reply-To: acl2-mtg@lists.cc.utexas.edu
Sender: owner-acl2-mtg@lists.cc.utexas.edu
X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN
Greetings,
This week, I will discuss a recent proof that I was doing with J, showing
equivalence between two different proof styles used for verifying operationally
modeled sequential programs in ACL2. The two styles are "inductive invariants"
and "clock functions". I will formalize each style of verification in ACL2 and
show that the styles are equivalent, that is, one can mechanically translate
proofs in one style to the proofs in the other.
We appreciate questions, comments, and suggestions.
Sandip.
---------------------------------------------------------------------------------
Here are the title and abstract of the talk:
TITLE: Proof Styles in Operational Semantics
ABSTRACT:
We relate two well-studied methodologies, use of inductive invariants and clock
functions, in deductive verification of operationally modeled sequential
programs. We prove that the two methodologies are equivalent in the following
sense: If the logic used is sufficiently expressive then one can mechanically
transform a proof of a program in one methodology to a proof in the other. Both
partial and total correctness are considered in this context. We also show that
the mechanical transformation is compositional in that different parts of a
program can be verified using different methodologies to achieve a complete
proof of the entire program. Our proof of equivalence has been mechanically
verified by the ACL2 theorem prover and we discuss automatic tools in the form
of ACL2 macros to carry out the mechanical transformation between the two
methodologies in the context of ACL2 theorem proving.
This is joint work with J Strother Moore.