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
- 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).
- Try to statically verify your previously written recipe card program with ESC/Java2.
Posted by David Aspinall 