Lecture 8: ESC/Java2

5 February 2009

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.

Read the rest of this entry »