[PRL] J Moore at MIT, tomorrow at 200

[Mitchell Wand]

From: CSAIL Event Calendar <eventcalendar at csail.mit.edu>
Sender: seminars-bounces at lists.csail.mit.edu
To: seminars at csail.mit.edu
Cc:=20
Subject: TALK:Thursday 10-28-04 Inductive Assertion-Style Proof
Date: Wed, 27 Oct 2004 15:04:39 -0400


Inductive Assertion-Style Proofs from Operational Semantics
Speaker: J Strother Moore
Speaker Affiliation: University of Texas at Austin
Host: Daniel Jackson
Host Affiliation: CSAIL   SDG

Date: 10-28-2004
Time: 2:00 PM - 3:00 PM
Refreshments: 1:45 PM
Location: 32 =96 G449 (Patil/Kiva)

Inductive Assertion-Style Proofs from Operational Semantics

Abstract:

Suppose you have a mechanical theorem prover for some logic and a
formal operational semantics, expressed in that logic, for some
programming language.  For example, in my case, I have the ACL2
(``Boyer-Moore'') theorem prover, which is a theorem prover for pure
Lisp, and an operational semantics for the bytecode of the Java
Virtual Machine.  The operational semantics is just a JVM, written in
pure Lisp.  Now suppose you want to prove a partial correctness
property of a program by the classic method of deriving ``verification
conditions'' from user-supplied assertions attached to the code.  Can
you do it with the tools at hand?  That is, can you do it without
writing a ``verification condition generator'' or other metatheoretic
formula transformer?  The answer is ``yes!''  In this talk I will show
you how.  I'll prove some theorems about simple Java methods by
annotating the bytecode produced by the Sun javac compiler.  The talk
will primarily be a demonstration of the JVM semantics in Lisp and the
use of the ACL2 theorem prover to manipulate it.  But buried amid the
details of these two rather complex systems will be a simple nugget of
information: how to use a mechanical theorem prover to prove theorems
via the Floyd-Hoare method directly from the operational semantics,
eliminating the need for special-purpose formula transformers.
        =20
Biography:
      =20
J Strother Moore holds the Admiral B.R. Inman Centennial Chair in
Computing Theory at the University of Texas at Austin.  He is also
chair of the department.  He is the author of many books and papers on
automated theorem proving and mechanical verification of computing
systems.  Along with Boyer he is a co-author of the Boyer-Moore
theorem prover and the Boyer-Moore fast string searching
algorithm. With Matt Kaufmann he is the co-author of the ACL2 theorem
prover.  Moore got his PhD from the University of Edinburgh in 1973
and his BS from MIT in 1970.  Moore was a founder of Computational
Logic, Inc.,  and served as its chief scientist for ten years.  He and
Bob Boyerwere awarded the 1991 Current Prize in Automatic Theorem
Proving by the American Mathematical Society.  In 1999 they were
awarded the Herbrand Award for their work in automatic theorem
proving.  Moore is a Fellow of the American Association for Artificial
Intelligence. =20

Host: Daniel Jackson

For more information please contact: Donna Kaufman, 617-253-4624, dkauf=
@mit.edu

_______________________________________________
Seminars mailing list
Seminars at lists.csail.mit.edu
http://lists.csail.mit.edu/mailman/listinfo/seminars