When: 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

Special Presentation

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 bytecode by the JVM model. I will discuss the general approach and show some examples, including theorems about sorting and simple multi-threaded applications.

<< Back