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 (ECOOP), 2008.
DOI : 10.1007/978-3-540-70592-5_17

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, Formal Methods for Components and Objects: 4th International Symposium, 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, Lecture Notes in Computer Science, vol.4355, 2007.
DOI : 10.1007/11955757_4

C. Breunesse and E. Poll, Verifying JML specifications with model fields, Formal Techniques for Java-like Programs, 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, Proceedings of the 8th Workshop on Formal Techniques for Java-like Programs (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

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

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

J. Filliâtre and C. Marché, Multi-prover Verification of C Programs, 6th International Conference on Formal Engineering Methods, 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, 19th International Conference on Computer Aided Verification, 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.

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

K. R. Leino and P. Müller, A Verification Methodology for Model Fields, 15th European Symposium on Programming, 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

K. R. Leino, A. Poetzsch-heffter, and Y. Zhou, Using data groups to specify and check side effects, PLDI. ACM, 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?, 3rd International Workshop on Aliasing, Confinement and Ownership in Object- Oriented Programming (IWACO), 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

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

E. Tushkanova, A. Giorgetti, C. Marché, and O. Kouchnarenko, Modular specification of Java programs, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00434452

E. Tushkanova, A. Giorgetti, C. Marché, and O. Kouchnarenko, Specifying generic Java programs: two case studies, Selected papers presented at LDTA'2010 workshop, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00525784

K. Zee, V. Kuncak, and M. Rinard, Full functional verification of linked data structures, ACM Conf. Programming Language Design and Implementation (PLDI), pp.349-361, 2008.