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.
Lecture 8: ESC/Java2
5 February 2009
Comments Off on Lecture 8: ESC/Java2 | 
Lecture log | 
Permalink
Posted by David Aspinall
