M. Barnett, B. E. Chang, R. Deline, B. Jacobs, and K. R. Leino, Boogie: A Modular Reusable Verifier for Object-Oriented Programs, FMCO 2005, pp.364-387, 2006.
DOI : 10.1007/11804192_17

B. Beckert, R. Hähnle, and P. H. Schmitt, Verification of Object-Oriented Software: The KeY Approach, LNCS, vol.4334, 2007.
DOI : 10.1007/978-3-540-69061-0

B. Beckert, S. Schlager, and P. H. Schmitt, An Improved Rule for While Loops in Deductive Program Verification, Proceedings, Seventh International Conference on Formal Engineering Methods (ICFEM), pp.315-329, 2005.
DOI : 10.1007/11576280_22

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Why3: Shepherd your herd of provers, Boogie 2011: First International Workshop on Intermediate Verification Languages, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

M. Brockschmidt, C. Otto, and J. Giesl, Modular termination proofs of recursive Java Bytecode programs by term rewriting, Proc. RTA '11, pp.155-170, 2011.

L. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS 2008, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

D. Distefano and M. J. Parkinson, jStar: towards practical verification for Java, Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applications, OOPSLA '08, pp.213-226, 2008.

J. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, 19th International Conference on Computer Aided Verification, pp.173-177, 2007.
DOI : 10.1007/978-3-540-73368-3_21

C. Fuhs, J. Giesl, M. Plücker, P. Schneider-kamp, and S. Falke, Proving Termination of Integer Term Rewriting, Proc. RTA '09, pp.32-47, 2009.
DOI : 10.1017/S1471068404002042

J. Giesl, P. Schneider-kamp, and R. Thiemann, AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework, Proc. IJCAR '06, LNAI 4130, pp.281-286, 2006.
DOI : 10.1007/11814771_24
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.2217

A. Kaldewaij, Programming: the derivation of algorithms, 1990.

I. T. Kassios, Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions, In FM, pp.268-283, 2006.
DOI : 10.1007/11813040_19

. Kiv-web-site, Competition solutions web presentation, 2011.

K. R. Leino, Dafny: An Automatic Program Verifier for Functional Correctness, LPAR-16, pp.348-370, 2010.
DOI : 10.1007/978-3-642-17511-4_20

K. R. Leino and M. Moskal, VACID-0: Verification of ample correctness of invariants of data-structures, edition 0, Proceedings of Tools and Experiments Workshop at VSTTE, 2010.

W. Mostowski, Formalisation and Verification of Java Card Security Properties in Dynamic Logic, Proceedings, Fundamental Approaches to Software Engineering (FASE) Conference 2005, pp.357-371, 2005.
DOI : 10.1007/978-3-540-31984-9_27

Y. Moy and C. Marché, The Jessie plugin for Deduction Verification in Frama-C ? Tutorial and Reference Manual, INRIA & LRI, 2011.

W. Reif, G. Schellhorn, K. Stenzel, and M. Balser, Structured Specifications and Interactive Proofs with KIV, Automated Deduction?A Basis for Applications, pp.13-39, 1998.
DOI : 10.1007/978-94-017-0435-9_1

P. H. Schmitt, M. Ulbrich, and B. Weiß, Dynamic Frames in Java Dynamic Logic, Revised Selected Papers, International Conference on Formal Verification of Object-Oriented Software, pp.138-152, 2010.
DOI : 10.1007/978-3-540-27815-3_37

K. Stenzel, A Formally Verified Calculus for Full Java Card, Algebraic Methodology and Software Technology (AMAST) 2004, Proceedings. Springer LNCS 3116, 2004.
DOI : 10.1007/978-3-540-27815-3_37