COSC5010: Formalizing the JVM in ACL2

Essentials

	Classroom:	EN 2101
	Time:	TTh 1:20-2:35 PM
	Textbooks:	Kaufmann, M., P. Manolios, and J S. Moore. Computer Aided Reasoning: An Approach. 2002. Copies are available from the instructor.
	Instructor:	John Cowles (cowles@uwyo.edu)
	Office Hours:	Tuesday: 3:00-4:00 Wednesday: 1:00-4:00 Thursday: 3:00-4:00
	Web page:	http://www.cs.uwyo.edu/~cowles/jvm-acl2/

Resources

• J Moore's introduction to "Proving theorems about Java and the JVM".
• Getting started with ACL2 programming. Note: This note assumes that you are in UT-Austin. Changes for running ACL2 in the University of Wyoming are found in assignment 1.
• iter-ack.lisp, an iterative version of Ackerman's function implemented in ACL2.
• proof-lesson1.lisp, a lesson in writing proofs in ACL2.
• proof-lesson2.lisp, a lesson in writing proofs in ACL2.
• proof-lesson3.lisp, a lesson in writing proofs in ACL2.
• proof-lesson4.lisp, a lesson in writing proofs in ACL2.
• proof-lesson5.lisp, a lesson in writing proofs in ACL2.
• m0.lisp, the M0 virtual machine model.
• m0-utilities.lisp, the M0 utility lemmas.
• defpun.lisp, the definition of defpun.
• m1.lisp, the M1 virtual machine model.
• m1-egs.lisp, examples of M1.
• m2.lisp, the M2 virtual machine model.
• m1-correct.lisp, M1 correctness without a clock.
• m1-correct1.lisp, Extended version of M1 correctness without a clock.
• m5.lisp, the M5 virtual machine model.
• m5-fact-eg.lisp, recursive static method for factorial on M5.
• m5-utilities.lisp, M5 utility lemmas.
• exam4-hint.lisp, a hint for exam question #4.

Assignments

• Assignment 1. This also contains some hints on running ACL2 at the University of Wyoming.
• Assignment 2, due Tuesday, February 3, 2004.
• Assignment 3.
• Assignment 4, due Tuesday, February 10, 2004.
• Assignment 5, due Tuesday, February 17, 2004.
• Assignment 6, due Tuesday, February 24, 2004.
• Assignment 7, due Tuesday, March 2, 2004.
• Assignment 8, due Thursday, March 11, 2004.
• Exam Question 1, due Tuesday, March 30, 2004.
• Exam Question 2, due Thursday, April 1, 2004.
• Exam Question 3, due Thursday, April 8, 2004.
• Exam Question 4, due Thursday, May 6, 2004. There is a hint for this problem.

Course Objectives

We will study a formal model of the Java Virtual Machine (JVM). The JVM is a stack-based, object-oriented, type-safe byte-code interpreter on which compiled Java programs are executed.

A ``formal model'' is a collection of mathematical formulas that describe precisely the functionality of (part of) the machine. The mathematical logic used to describe the machine is Pure Lisp. The subset of Lisp used is quite small (compared to all of Common Lisp).

This course is not about the Java programming language but the underlying byte-code machine.

The Java Virtual Machine Specification is available at http://java.sun.com/docs/books/vmspec/2nd-edition/html/VMSpecTOC.doc.html.

The subset of Lisp used is called ACL2. ACL2 is both a programming language in which you can model computer systems and a tool to help you prove properties of those models. ACL2 is described at http://www.cs.utexas.edu/users/moore/acl2/acl2-doc.html.