E. Albert, R. Bubel, S. Genaim, R. Hähnle, G. Puebla et al., Verified resource guarantees using COSTA and KeY, Proceedings of the 20th ACM SIGPLAN workshop on Partial evaluation and program manipulation, PERM '11, pp.73-76, 2011.
DOI : 10.1145/1929501.1929513
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.186.2576

A. W. Appel, Foundational proof-carrying code, LICS 2001, pp.247-256, 2001.
DOI : 10.1109/lics.2001.932501
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.2076

M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry et al., A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, CPP'11, pp.135-150, 2011.
DOI : 10.1145/1217856.1217859
URL : https://hal.archives-ouvertes.fr/hal-00639130

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

M. Barnett, K. R. Leino, and W. Schulte, The Spec# Programming System: An Overview, CASSIS'04, pp.49-69, 2004.
DOI : 10.1007/978-3-540-30569-9_3

F. Besson, P. Cornilleau, and T. Jensen, Why3 and Coq source of the development, 2012.

F. Besson, P. Cornilleau, and D. Pichardie, Modular SMT Proofs for Fast Reflexive Checking Inside Coq, CPP'11, pp.151-166, 2011.
DOI : 10.1016/j.jal.2007.07.003
URL : https://hal.archives-ouvertes.fr/hal-00646960

F. Besson, T. Jensen, D. Pichardie, and T. Turpin, Certified Result Checking for Polyhedral Analysis of Bytecode Programs, TGC'10, pp.253-267, 2010.
DOI : 10.1007/978-3-642-15640-3_17
URL : https://hal.archives-ouvertes.fr/inria-00537816

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Why3: Shepherd your herd of provers, Boogie 2011, pp.53-64, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

S. Böhme and T. Nipkow, Sledgehammer: Judgement Day, IJCAR'10, pp.107-121, 2010.
DOI : 10.1007/978-3-642-14203-1_9

T. Bouton, D. C. Oliveira, D. Déharbe, and P. Fontaine, veriT: An Open, Trustable and Efficient SMT-Solver, CADE'09, pp.151-156, 2009.
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634

D. Cachera, T. Jensen, D. Pichardie, and V. Rusu, Extracting a data flow analyser in constructive logic, Theoretical Computer Science, vol.342, issue.1, pp.56-78, 2005.
DOI : 10.1016/j.tcs.2005.06.004
URL : https://hal.archives-ouvertes.fr/inria-00564633

B. E. Chang, A. Chlipala, G. C. Necula, and R. R. Schneck, The open verifier framework for foundational verifiers, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation , TLDI '05, pp.1-12, 2005.
DOI : 10.1145/1040294.1040295

E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal et al., VCC: A Practical System for Verifying Concurrent C, TPHOLs'09, pp.23-42, 2009.
DOI : 10.1007/978-3-540-74591-4_15

P. Cornilleau, Prototyping static analysis certification using Why3, 2012.

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/inria-00528590

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

D. Demange, T. P. Jensen, and D. Pichardie, A Provably Correct Stackless Intermediate Representation for Java Bytecode, APLAS, pp.97-113, 2010.
DOI : 10.1007/978-3-642-17164-2_8
URL : https://hal.archives-ouvertes.fr/inria-00414099

M. Fähndrich and K. R. Leino, Declaring and checking non-null types in an object-oriented language, OOPSLA'03, pp.302-312, 2003.

C. Flanagan and K. R. Leino, Houdini, an Annotation Assistant for ESC/Java, LNCS, vol.2021, pp.500-517, 2001.
DOI : 10.1007/3-540-45251-6_29

C. Flanagan, K. R. Leino, M. Lillibridge, G. Nelson, J. B. Saxe et al., Extended static checking for Java, PLDI'02, pp.234-245, 2002.

P. Fontaine, Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class, VERIFY, volume 259 of CEUR Workshop Proceedings. CEUR-WS.org, 2007.

L. Hubert, N. Barré, F. Besson, D. Demange, T. P. Jensen et al., Sawja: Static Analysis Workshop for Java, FoVeOOS, pp.92-106, 2010.
DOI : 10.1023/B:JARS.0000021015.15794.82
URL : https://hal.archives-ouvertes.fr/inria-00504047

L. Hubert, T. Jensen, and D. Pichardie, Semantic foundations and inference of nonnull annotations, FMOODS'08, pp.132-149, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00332356

B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx et al., VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java, NFM'11, pp.41-55, 2011.
DOI : 10.1007/11691372_19

G. Klein and T. Nipkow, Verified bytecode verifiers, Theoretical Computer Science, vol.298, issue.3, pp.583-626, 2003.
DOI : 10.1016/S0304-3975(02)00869-1

X. Leroy, Java bytecode verification: Algorithms and formalizations, Journal of Automated Reasoning, vol.30, issue.3/4, pp.235-269, 2003.
DOI : 10.1023/A:1025055424017
URL : https://hal.archives-ouvertes.fr/hal-01499939

X. Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, POPL'06, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

T. Lindholm and F. Yellin, Java Virtual Machine Specification, 1999.

C. Marché and A. Tafat, Weakest Precondition Calculus, Revisited using Why3, 2012.

G. C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.106-119, 1997.
DOI : 10.1145/263699.263712

G. C. Necula and P. Lee, Proof generation in the Touchstone theorem prover 34. D. Pichardie. Interprétation abstraite en logique intuitionniste: extraction d'analyseurs Java certifiés, CADE'00, pp.25-44, 2000.

R. Piskac, L. M. De-moura, and N. Bjørner, Deciding Effectively Propositional Logic Using DPLL and Substitution Sets, Journal of Automated Reasoning, vol.53, issue.6, pp.401-424, 2010.
DOI : 10.1007/s10817-009-9161-6

G. Sutcliffe, The 5th IJCAR Automated Theorem Proving System Competition - CASC-J5, pp.75-89, 2011.

E. D. Tempero, J. Noble, and H. Melton, How Do Java Programs Use Inheritance? An Empirical Study of Inheritance in Java Software, ECOOP'08, pp.667-691, 2008.
DOI : 10.1007/978-3-540-70592-5_28

H. Wasserman and M. Blum, Software reliability via run-time result-checking, Journal of the ACM, vol.44, issue.6, pp.826-849, 1997.
DOI : 10.1145/268999.269003