Lecture 5: ESC/Java2 – The Java Extended Static Checker

25 January 2010

ESC/Java2: a verification tool combining several analysis techniques (types, dataflow, proof). An overview of the checks it performs: exception freedom for common exceptions (null pointers, array indices, class casts). The lack of soundness and completeness: false positives and defects missed. Some further and specialised annotations extending core JML (non_null, unreachable, modifies, pure). Specification inheritance.

Links: Slides; ESC/Java2 downloads.

Homework

  1. Try ESC/Java on some of the example files and some Java (1.4) programs of your own (see below how to run ESC/Java2 on DICE).
  2. Try to statically verify your previously written recipe card program with ESC/Java2.

Read the rest of this entry »