Final Year Project Report Automatic lb and Completeness Warnings in ESC Java2 Barry Denby A thesis submitted in part fulfilment of the degree of BA BSc hons in Computer Science Supervisor Dr Joseph Kiniry Moderator Dr Alexey Lastovetsky UCD School of Computer Science and Informatics College of Engineering Mathematical and Physical Sciences University College Dublin April 7 2006 Table of Contents Nbstrac l aneas eb ica Bee ee ee ee a eS ce GOH Ww
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
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