L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry et al., An overview of JML tools and applications, FMICS 03, p.7389, 2003.
DOI : 10.1007/s10009-004-0167-4

J. Chrzaszcz, Implementing Modules in the Coq System, TPHOLs'03, p.270286, 2003.
DOI : 10.1007/10930755_18

D. R. Cok, Adapting JML to generic types and Java 1.6, SAVCBS '08, p.2734, 2008.

J. Filliâtre and N. Magaud, Certication of sorting algorithms in the Coq system, Theorem Proving in Higher Order Logics: Emerging Trends, 1999.

J. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus platform for deductive program verication, CAV'07, p.173177, 2007.

J. Kanig and J. Filliâtre, Who: A Verier for Eectful Higher-order Programs, In ACM SIGPLAN Workshop on ML, 2009.

G. T. Leavens and Y. Cheon, Design by Contract with JML. Available from http, 2006.

C. Marché, Towards modular algebraic specications for pointer programs: a case study, Rewriting, Computation and Proof, p.235258, 2007.

C. Marché, The Krakatoa tool for deductive verication of Java programs . Winter School on Object-Oriented Verication, 2009.

J. Mitchell, S. Meldal, and N. Madhav, 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

S. M. Shaner, G. T. Leavens, and D. A. Naumann, Modular verication of higher-order methods with mandatory calls specied by model programs, Proceedings of OOPSLA'07, p.351368, 2007.

K. Stenzel, H. Grandy, and W. Reif, Verication of Java programs with generics, AMAST'08, number 5140 in LNCS, p.315329, 2008.

A. Tafat, S. Boulmé, and C. Marché, A renement methodology for objectoriented programs, 2009.

M. Ulbrich, Software verication for Java 5. Diplomarbeit, Fakultät für Informatik, 2007.