J. Barnes, Programming in Ada 2012, 2014.
DOI : 10.1017/CBO9781139696616

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

P. Baudin, J. C. Filliâtre, C. Marché, B. Monate, Y. Moy et al., ACSL: ANSI/ISO C Specification Language, version 1, 2013.

L. Bulwahn, The New Quickcheck for Isabelle, pp.92-108, 2012.
DOI : 10.1007/978-3-642-35308-6_10

L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry et al., An overview of JML tools and applications, International Journal on Software Tools for Technology Transfer, vol.box, issue.3, pp.212-232, 2005.
DOI : 10.1007/s10009-004-0167-4

J. Burghardt, J. Gerlach, T. Lapawczyk, A. Carben, L. Gu et al., ACSL by example, towards a verified C standard library. version 11.11 for Frama-C Sodium, Tech. rep., Fraunhofer FOKUS, 2015.

P. Chalin, Logical foundations of program assertions: what do practitioners want?, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), pp.383-393, 2005.
DOI : 10.1109/SEFM.2005.26

P. Chalin, Reassessing JML's logical foundation, Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP'05, 2005.

R. Chapman and F. Schanda, Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK, ITP. LNCS, pp.17-26, 2014.
DOI : 10.1007/978-3-319-08970-6_2

M. Christakis, K. R. Leino, P. Müller, and V. Wüstholz, Integrated Environment for Diagnosing Verification Errors, 2016.
DOI : 10.1007/978-3-662-49674-9_25

M. Clochard, Automatically Verified Implementation of Data Structures Based on AVL Trees, VSTTE. LNCS, pp.167-180, 2014.
DOI : 10.1007/978-3-319-12154-3_11
URL : https://hal.archives-ouvertes.fr/hal-01067217

M. Clochard, J. C. Filliâtre, C. Marché, and A. Paskevich, Formalizing Semantics with an Automatic Program Verifier, VSTTE. LNCS, pp.37-51, 2014.
DOI : 10.1007/978-3-319-12154-3_3
URL : https://hal.archives-ouvertes.fr/hal-01067197

M. Clochard, C. Marché, and A. Paskevich, Verified programs with binders, Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages meets Program Verification, PLPV '14, 2014.
DOI : 10.1145/2541568.2541571
URL : https://hal.archives-ouvertes.fr/hal-00913431

D. R. Cok, OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse, Electronic Proceedings in Theoretical Computer Science, vol.149, pp.79-92, 2014.
DOI : 10.4204/EPTCS.149.8

L. Correnson and J. Signoles, Combining Analyses for C Program Verification, FMICS. LNCS, pp.108-130, 2012.
DOI : 10.1007/978-3-642-32469-7_8

M. Delahaye, N. Kosmatov, and J. Signoles, Common specification language for static and dynamic analysis of C programs, Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC '13, pp.1230-1235, 2013.
DOI : 10.1145/2480362.2480593
URL : https://hal.archives-ouvertes.fr/hal-00853721

C. Dross, J. C. Filliâtre, and Y. Moy, Correct Code Containing Containers, TAP. LNCS, pp.102-118, 2011.
DOI : 10.1145/1375581.1375624
URL : https://hal.archives-ouvertes.fr/hal-00777683

C. Dross and Y. Moy, Abstract Software Specifications and Automatic Proof of Refinement
DOI : 10.1007/978-3-319-33951-1_16

J. L. Dufour, Formal Methods Applied to Complex Systems, chap. B Extended to Floating- Point Numbers: Is it Sufficient for Proving Avionics Software?, 2014.

J. C. Filliâtre, L. Gondelman, and A. Paskevich, The spirit of ghost code, Formal Methods in System Design, 2016.

J. C. Filliâtre and C. Marché, Multi-prover Verification of C Programs, In: ICFEM. pp, pp.15-29, 2004.
DOI : 10.1007/978-3-540-30482-1_10

J. C. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, CAV. LNCS, pp.173-177, 2007.
DOI : 10.1007/978-3-540-73368-3_21

J. C. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, ESOP. LNCS, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

S. Gao, J. Avigad, and E. M. Clarke, Delta-complete decision procedures for satisfiability over the reals, 2012.

D. Hauzar, C. Marché, and Y. Moy, Counterexamples from Proof Failures in SPARK, SEFM. LNCS, 2016.
DOI : 10.1007/978-3-662-49674-9_25
URL : https://hal.archives-ouvertes.fr/hal-01314885

B. Jacobs, C. Marché, and N. Rauch, Formal Verification of a Commercial Smart Card Applet with Multiple Tools, AMAST. LNCS, 2004.
DOI : 10.1007/978-3-540-27815-3_21

A. Jakobsson, N. Kosmatov, and J. Signoles, Rester statique pour devenir plus rapide, plus précis et plus mince, p.JFLA, 2015.

J. Kanig, R. Chapman, C. Comar, J. Guitton, Y. Moy et al., Explicit Assumptions - A Prenup for Marrying Static and Dynamic Program Verification, TAP. LNCS, pp.142-157, 2014.
DOI : 10.1007/978-3-319-09099-3_11

F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, Frama-C: A software analysis perspective. Formal Aspects of Computing pp, pp.1-37, 2015.

E. Kneuss, I. Kuraj, V. Kuncak, and P. Suter, Synthesis modulo recursive functions, pp.407-426, 2013.

N. Kosmatov, G. Petiot, and J. Signoles, An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs, RV. LNCS, pp.167-182, 2013.
DOI : 10.1007/978-3-642-40787-1_10

N. Kosmatov and J. Signoles, A Lesson on Runtime Assertion Checking with Frama-C, RV. LNCS, pp.386-399, 2013.
DOI : 10.1007/978-3-642-40787-1_29

N. Kosmatov and J. Signoles, Runtime assertion checking and its combinations with static and dynamic analyses -tutorial synopsis, pp.165-168, 2014.

G. T. Leavens, Y. Cheon, C. Clifton, C. Ruby, and D. R. Cok, How the design of JML accomodates both runtime assertion checking and formal verification, 2003.

K. R. Leino, Automating Induction with an SMT Solver, pp.315-331, 2012.
DOI : 10.1007/978-3-540-45085-6_28

K. R. Leino and V. Wüstholz, The Dafny Integrated Development Environment, Electronic Proceedings in Theoretical Computer Science, pp.3-15, 2014.
DOI : 10.4204/EPTCS.149.2

C. Marché, C. Paulin-mohring, and X. Urbain, The KRAKATOA tool for certification of JAVA/- JAVACARD programs annotated in JML, Journal of Logic and Algebraic Programming, vol.58, pp.1-2, 2004.

J. W. Mccormick and P. C. Chapin, Building High Integrity Applications with SPARK, 2015.
DOI : 10.1017/CBO9781139629294

B. Meyer, Object-Oriented Software Construction, 1988.

G. Petiot, N. Kosmatov, B. Botella, A. Giorgetti, and J. Julliand, Your Proof Fails? Testing Helps to Find the Reason, TAP. LNCS, 2016.
DOI : 10.1007/978-3-662-49674-9_25

J. Signoles, Software Architecture of Code Analysis Frameworks Matters: The Frama-C Example, Electronic Proceedings in Theoretical Computer Science, vol.187, pp.86-96, 2015.
DOI : 10.4204/EPTCS.187.7

J. Tschannen, C. Furia, M. Nordio, and B. Meyer, Program Checking with Less Hassle, pp.149-169, 2014.
DOI : 10.1007/978-3-642-54108-7_8

J. Tschannen, C. A. Furia, M. Nordio, and N. Polikarpova, AutoProof: Auto-Active Functional Verification of Object-Oriented Programs, pp.566-580, 2015.
DOI : 10.1007/978-3-662-46681-0_53