Message-ID: <4E06A937DADC3842ACE4D3A1096A9EAC568277@janus.EECS.Berkeley.EDU> From: George Necula <necula@EECS.Berkeley.EDU> Date: Thu, 5 Dec 2002 12:44:47 -0800 X-Spam-Report: SPAM: -------------- Start EECS SpamAssassin results ----------- SPAM: The EECS department SpamAssassin FAQ is at SPAM: http://iris.eecs.berkeley.edu/idsg/SpamAssassin SPAM: SPAM: Content analysis details: (1.30 hits, 5 required) SPAM: EXCHANGE_SERVER (-0.1 points) Came via Internet Mail Service plugin SPAM: SUBJ_MISSING (0.3 points) Subject: is empty or missing SPAM: SPAM_PHRASE_00_01 (0.8 points) BODY: Spam phrases score is 00 to 01 (low) SPAM: CARRIAGE_RETURNS (0.3 points) RAW: Message contains a lot of ^M characters SPAM: SPAM: ----------------- End of SpamAssassin results ------------------ Sender: owner-softquality@EECS.Berkeley.EDU Precedence: bulk J. Strother Moore from UT Austin will talk today at 2pm in Soda 380 about his project on the verification of Java and the JVM. See the URL below: George. 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. 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. Bio: 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.
This archive was generated by hypermail 2b30 : 12/07/02 PST