COSC5010: Formalizing the JVM in ACL2
Essentials

Classroom:

EN 2101


Time:

TTh 1:202: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:004:00 
Wednesday:  1:004:00 
Thursday:  3:004:00 


Web page:

http://www.cs.uwyo.edu/~cowles/jvmacl2/

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 UTAustin. Changes for running ACL2 in
the University of Wyoming are found in
assignment 1.
 iterack.lisp, an iterative
version of Ackerman's function implemented in ACL2.
 prooflesson1.lisp, a lesson
in writing proofs in ACL2.
 prooflesson2.lisp, a lesson
in writing proofs in ACL2.
 prooflesson3.lisp, a lesson
in writing proofs in ACL2.
 prooflesson4.lisp, a lesson
in writing proofs in ACL2.
 prooflesson5.lisp, a lesson
in writing proofs in ACL2.
 m0.lisp, the M0 virtual machine model.
 m0utilities.lisp, the M0
utility lemmas.
 defpun.lisp, the definition of defpun.
 m1.lisp, the M1 virtual machine model.
 m1egs.lisp, examples of M1.
 m2.lisp, the M2 virtual machine model.
 m1correct.lisp, M1 correctness without a clock.
 m1correct1.lisp, Extended
version of M1 correctness without a clock.
 m5.lisp, the M5 virtual machine model.
 m5facteg.lisp, recursive
static method for factorial on M5.
 m5utilities.lisp, M5
utility lemmas.
 exam4hint.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 stackbased, objectoriented, typesafe
bytecode 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 bytecode machine.
The Java Virtual Machine Specification is available at
http://java.sun.com/docs/books/vmspec/2ndedition/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/acl2doc.html.