J Strother Moore
An Executable Formal Model of the Java Virtual Machine
Wednesday, May 5, 2004
Building 3 Auditorium - 3:30 PM
(Refreshments at 3:00 PM)

Dr. J Strother Moore, will talk about An Executable Formal Model of the Java Virtual Machine. In this talk Dr. Moore will sketch a model of the JVM that includes dynamic class loading, class initialization and synchronization via monitors. The model is written in a first-order functional programming language with a formal axiomatic semantics. Thus, the model is both a conventional executable JVM emulator and a mathematical description of the machine. As an emulator, the model executes most J2ME Java programs that do not use any I/O or floating point operations. The formal language in which the model is written is supported by a mechanized theorem proving system. Using this system we can mechanically prove theorems about both the model and about bytecode programs executed on it. The fact that the model has dual use increases our confidence in its correctness and opens the door to other possibilities, like symbolic execution of Java and the production of a Java verification system.

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 seaching algorithm. With Matt Kaufmann, he is the co-author of the ACL2 theorem prover. Moore got his PhD from 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.

IS&T Colloquium Committee Host: Karen Moe
Karen.L.Moe@nasa.gov

Sign language interpreter upon request: 301-286-8313
Request future announcements: kjeter@pop200.gsfc.nasa.gov