Friday, October 04, 10:00 a.m.- 11:30 a.m.
Where: 4623 Wean Hall
J. Strother Moore, Professor and Chair, Department of Computer Sciences, University of Texas at Austin
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 bytecode by the JVM model. I will discuss the general
approach and show some examples, including theorems about sorting and
simple multi-threaded applications.