ESC Java2 Implementation Notes David R Cok cok frontiernet net Joseph R Kiniry joseph kiniry ucd ie Dermot Cochran Dermot Cochran ucd ie October 2008 Abstract ESC Java2 is a tool for statically checking program specifications It expands significantly upon ESC Java on which it is built It is consistent with the definition of JML and of Java 1 4 It adds additional static checking to that in ESC Java most significantly it adds support for checking frame cond
Soundness and Completeness Warnings in ESC Java2 Joseph R Kiniry Alan E Morkan and Barry Denby School of Computer Science and Informatics University College Dublin Belfield Dublin 4 Ireland ABSTRACT Usability is a key concern in the development of verifica tion tools In this paper we present an usability extension for the verification tool ESC Java2 This enhancement is not achieved through extensions to the underlying logic or calculi of ESC Java2 but instead we fo
Soundness and Completeness Warnings in ESC Java2 Joseph R Kiniry Alan E Morkan and Barry Denby School of Computer Science and Informatics University College Dublin Belfield Dublin 4 Ireland ABSTRACT Usability is a key concern in the development of verification tools In this paper we present an usability extension for the verifica tion tool ESC Java2 This enhancement is not achieved through extensions to the underlying logic or calculi of ESC Java2 but in stead we