*** Please note the time and place change, only for this week. ***

-----------------------------------------------------------------------
TDS Seminar TDS Seminar TDS Seminar TDS Seminar TDS Seminar TDS Seminar
-----------------------------------------------------------------------

Title:    Proving Theorems about Java and the JVM

Speaker:  J Strother Moore
          Department of Computer Sciences
          University of Texas at Austin

Date:     Friday, October 11, 2002
Time:     Refreshments 12:30 pm, Talk: 12:45 pm
Place:    NE43-518

Abstract:
I will explain how the latest version of the Boyer-Moore theorem prover,
ACL2, is used to prove theorems about Java methods. ACL2 may be thought of
as a theorem prover for functional Common Lisp. We model the Java Virtual
Machine (JVM) operationally, e.g., as a Lisp function. We prove theorems
about Java methods by compiling the methods with javac and proving theorems
about the execution of the resulting byte code by the JVM model. I will
discuss the general approach and show some examples. The examples will deal
with Java's int arithmetic, simple control, including recursion, object
creation and modification in the heap, thread creation, and mutual
exclusion via monitors.

Biography:
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
Boyer were 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.

Host: Michael Ernst    

------------------------------------------------------------------------