An overview of JML tools and applications, FMICS 03, p.7389, 2003. ,
DOI : 10.1007/s10009-004-0167-4
Implementing Modules in the Coq System, TPHOLs'03, p.270286, 2003. ,
DOI : 10.1007/10930755_18
Adapting JML to generic types and Java 1.6, SAVCBS '08, p.2734, 2008. ,
Certication of sorting algorithms in the Coq system, Theorem Proving in Higher Order Logics: Emerging Trends, 1999. ,
The Why/Krakatoa/Caduceus platform for deductive program verication, CAV'07, p.173177, 2007. ,
Who: A Verier for Eectful Higher-order Programs, In ACM SIGPLAN Workshop on ML, 2009. ,
Design by Contract with JML. Available from http, 2006. ,
Towards modular algebraic specications for pointer programs: a case study, Rewriting, Computation and Proof, p.235258, 2007. ,
The Krakatoa tool for deductive verication of Java programs . Winter School on Object-Oriented Verication, 2009. ,
An extension of standard ML modules with subtyping and inheritance, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '91, p.270278 ,
DOI : 10.1145/99583.99620
Modular verication of higher-order methods with mandatory calls specied by model programs, Proceedings of OOPSLA'07, p.351368, 2007. ,
Verication of Java programs with generics, AMAST'08, number 5140 in LNCS, p.315329, 2008. ,
A renement methodology for objectoriented programs, 2009. ,
Software verication for Java 5. Diplomarbeit, Fakultät für Informatik, 2007. ,