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.