This is some documentation on how to get started with some of the CS 378 tools. It is not complete, but it should still be helpful.

KeY

KeY is a theorem prover built with the intent of proving theorems about Java functions. To get started with KeY, you can run the following commands:

cd /v/filer4b/projects-browne/uvv-fall2008/KeY
bin/startProver

After starting the program, you want to load your java file. You'll need to select some functions, and probably some proof goals. After you do this, you can hit the "play" button near the top left of the prover and KeY will attempt to prove the goal. Note that automatic proofs are rather difficult to obtain, but it works pretty well for the difficulty of the task.

The best tutorial I've found for KeY is in chapter 10 of a $100 book available for download from a UTCS machine named Verification of Object-Oriented Software: The KeY Approach, Chapter 10, Using KeY. The second best tutorial is probably: quicktour. The accompanying source can be found here source. If you're a graduate student, you'll probably want to start reading the tutorial from the beginning. If you're an undergrad, you might enjoy starting with the more concrete things around page 5.

ESC Java 2 Model Checking Tools

The ESC Java 2 tools were built to check JML annotations. To get started with the ESC Java 2 tools, you can run the following commands:

cd /v/filer4b/projects-browne/uvv-fall2008/ESCJava
./quicktest

You can run escjava2 or escj with various flags on your java files to model check them.

JML Compiler and Runtime Assertion Checker

You can download a compiler that turns JML annotations into runtime assertion checks. This means that your JML invariants, preconditions, etc. can all be checked during runtime. This tool can be downloaded from sourceforge [link]

JPF

Java Path Finder is a model checker for Java. According to their website, it can handle programs of length up to about 10,000 LOC (lines of code).

Note that we did not use jpf in the fall 2008 version of the class.

The run JPF you can type the following

cd /v/filer4b/projects-browne/uvv-fall2008/JPF
bin/jpf

Blast

Blast is a model checker for C. The Third Chapter of the Blast Manual contains a tutorial that will help you get started using Blast.

The following code provides a sample execution of blast. Note that blast catches the fact that I've omitted a return statement from the main function, while gcc and g++ said nothing. Obviously model checking is more than finding missing return statements, but it's a sign that the tool is doing at least something useful. By running the commands, you can see that 11 nodes are created. A BDD (Binary Decision Diagram) is just a way of representing the states that we've discusses in class. The setenv command works if your shell is tcsh or csh. If you're using bash, you need to use the export version of it.

cd /v/filer4b/projects-browne/uvv-fall2008/Blast-2.5
setenv PATH ${PATH}:/v/filer4b/projects-browne/uvv-fall2008/Blast-2.5/blast/bin
blast/bin/pblast.opt example.c -main main -L ERROR

An alternative to Blast is Magic, but due to compliation problems, it hasn't been enabled yet. If you have a compelling reason to use Magic, let me know, and we can figure it out.

ObjectBench

ObjectBench is a tool suite that can model programs. In fact, you can write the model, and ObjectBench will generate code in Java that implements that model. When Dr. Browne refers to "writing a model and then generating code from that model," he is refering to the use of this tool.

The instructions for using ObjectBench look something like the following, but I personally have been getting X11 errors which prevent me from starting the tutorial. To run ObjectBench do the following:
  1. Login to one of the department Sun machines by sitting in front of it and typing on its very keyboard.
  2. execute in your shell: source /projects/ses.new/sun/ob3.1-3/sescsh_Objectbench
  3. execute in your shell: /projects/ses.new/sun/ob3.1-3/Objectbench_31_sun4SunOS5/obTraining

Warren A. Hunt, Jr.'s and Laurence Pierre's Model Checker for ACL2

To load Hunt's model checker, log into a UTCS machine and type:
/p/bin/acl2
(include-book "/v/filer4b/projects-browne/uvv-fall2008/mc/mc7")

If you find mistakes (and even better corrections), please let me know, so that I can forward the filtered information to Dr. Hunt. This model checker has been around for many years, and although it's just a "toy", Dr. Hunt does have a desire to fix whatever bugs may exist.

An example that can be found in the file /v/filer4b/projects-browne/uvv-fall2008/mc/mc7.lisp is as follows. Remember that acl2/LISP code is in prefix notation (as opposed to infix notation, which is what most procedural programming languages use). You can think of assign as the = operator and @ as just returning the value of the variable that it takes as its operator.

(assign
 kripke
 '(;; Initial state
   ()  ; Right now, we don't care
   ;; Transition Relation
   ((a a b c)
    (b     c)
    (c a    ))
   ;;
   ((a a)
    (b b)
    (c c)
    (p a b  )
    (q     c)
    (r      ))))

; Play around with making your own forms to gain understanding

(assign
 form
 '(and p (EX c)))

(eval-mc (@ form) (@ kripke))