M. Barnett, K. R. Leino, and W. Schulte, The Spec# Programming System: An Overview, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pp.49-69, 2004.
DOI : 10.1007/978-3-540-30569-9_3

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

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

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

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

R. Bornat, Proving Pointer Programs in Hoare Logic, Mathematics of Program Construction, pp.102-126, 2000.
DOI : 10.1007/10722010_8

J. Burghardt, J. Gerlach, L. Gu, K. Hartig, H. Pohl et al., ACSL by example , towards a verified C standard library, 2011.

D. R. Cok, J. Kiniry, E. Esc-/-java2-uniting, J. Java, . G. In et al., ESC/Java2: Uniting ESC/Java and JML, Lecture Notes in Computer Science, vol.3362, pp.108-128, 2004.
DOI : 10.1007/978-3-540-30569-9_6

M. Dahlweid, M. Moskal, T. Santen, S. Tobies, and W. Schulte, VCC: Contract-based modular verification of concurrent C, 2009 31st International Conference on Software Engineering, Companion Volume, pp.429-430, 2009.
DOI : 10.1109/ICSE-COMPANION.2009.5071046

E. W. Dijkstra, A discipline of programming. Series in Automatic Computation, 1976.

J. Filliâtre, Verification of non-functional programs using interpretations in type theory, Journal of functional Programming, vol.13, issue.4, pp.709-745, 2003.
DOI : 10.1017/S095679680200446X

J. Filliâtre and N. Magaud, Certification of Sorting Algorithms in the System Coq, Theorem Proving in Higher Order Logics: Emerging Trends, 1999.

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

R. W. Floyd, Assigning meanings to programs, of Proceedings of Symposia in Applied Mathematics, pp.19-32, 1967.
DOI : 10.1090/psapm/019/0235771

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.2392

G. T. Leavens, K. R. Leino, and P. Müller, Specification and verification challenges for sequential object-oriented programs. Formal Aspects of Computing, 2007.

K. R. Leino, Dafny: An Automatic Program Verifier for Functional Correctness, 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.

Y. Moy, Automatic Modular Static Safety Checking for C Programs, 2009.

A. Tafat, S. Boulmé, and C. Marché, A Refinement Methodology for Object-Oriented Programs, Formal Verification of Object-Oriented Software , Papers Presented at the International Conference, pp.143-159, 2010.
DOI : 10.1006/inco.1996.2613
URL : https://hal.archives-ouvertes.fr/inria-00534336