J. Abrial, The B-Book, assigning programs to meaning, 1996.

R. Back and J. Wright, Refinement Calculus: A Systematic Introduction, 1998.
DOI : 10.1007/978-1-4612-1674-2

A. Banerjee, D. A. Naumann, and S. Rosenberg, Regional Logic for Local Reasoning about Global Invariants, European Conference on Object-Oriented Programming, 2008.
DOI : 10.1007/978-3-540-70592-5_17
URL : http://cis.ksu.edu/~ab/Publications/rllrgi.pdf

M. Barnett, R. Deline, M. Fähndrich, K. R. Leino, and W. Schulte, Verification of Object-Oriented Programs with Invariants., The Journal of Object Technology, vol.3, issue.6, pp.27-56, 2004.
DOI : 10.5381/jot.2004.3.6.a2

M. Barnett, R. Deline, B. Jacobs, B. E. Chang, 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, 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, 2008.

P. Behm, P. Benoit, A. Faivre, and J. Meynadier, M??t??or: A Successful Application of B in a Large Project, Formal Methods'99, pp.348-387, 1999.
DOI : 10.1007/3-540-48119-2_22

S. Boulmé and M. Potet, Interpreting Invariant Composition in the B Method Using the Spec# Ownership Relation: A Way to Explain and Relax B Restrictions, LNCS, vol.4355, 2007.
DOI : 10.1007/11955757_4

C. Breunesse and E. Poll, Verifying JML specifications with model fields, FTfJP'03, 2003.

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

J. Charles, Adding native specifications to JML, FTfJP'06, 2006.

Y. Cheon, G. Leavens, M. Sitaraman, and S. Edwards, Model variables: cleanly supporting abstraction in design by contract, Software: Practice and Experience, vol.36, issue.6, pp.583-599, 2005.
DOI : 10.1002/spe.649

A. P. Darvas, Reasoning About Data Abstraction in Contract Languages, 2009.

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

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

G. T. Leavens, K. R. Leino, and P. Müller, Specification and verification challenges for sequential object-oriented programs. Formal Aspects of Computing, 2007.
DOI : 10.1007/s00165-007-0026-7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.70.6538

K. R. Leino, Data groups: Specifying the modification of extended state, OOPSLA'98, pp.144-153, 1998.

K. R. Leino and P. Müller, A Verification Methodology for Model Fields, ESOP'06, pp.115-130, 2006.
DOI : 10.1002/cpe.713

K. R. Leino and G. Nelson, Data abstraction and information hiding, ACM Transactions on Programming Languages and Systems, vol.24, issue.5, pp.491-553, 2002.
DOI : 10.1145/570886.570888
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.6657

K. R. Leino, A. Poetzsch-heffter, and Y. Zhou, Using data groups to specify and check side effects, PLDI'02, 2002.
DOI : 10.1145/512529.512559
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.138.8083

C. Morgan, Programming from specifications, 1994.

M. Parkinson, Class invariants: The end of the road? In IWACO'07, 2007.

J. C. Reynolds, Separation logic: a logic for shared mutable data structures, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, 2002.
DOI : 10.1109/LICS.2002.1029817

A. Tafat, S. Boulmé, and C. Marché, A refinement approach for correct-by-construction object-oriented programs, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00491835

J. Talpin and P. Jouvelot, Abstract, Journal of Functional Programming, vol.78, issue.03, pp.245-271, 1992.
DOI : 10.1145/322123.322135
URL : https://hal.archives-ouvertes.fr/hal-00730926

M. Tofte and J. Talpin, Region-Based Memory Management, Information and Computation, vol.132, issue.2, pp.109-176, 1997.
DOI : 10.1006/inco.1996.2613
URL : http://doi.org/10.1006/inco.1996.2613

K. Zee, V. Kuncak, and M. Rinard, Full functional verification of linked data structures, PLDI'08, pp.349-361, 2008.