C. Barrett, C. Tinelli, and . Cvc3, CVC3, 19th International Conference on Computer Aided Verification, pp.298-302, 2007.
DOI : 10.1007/978-3-540-73368-3_34

J. Berdine, C. Calcagno, and P. W. O-'hearn, Smallfoot: Modular Automatic Assertion Checking with Separation Logic, International Symposium on Formal Methods for Components and Objects, pp.115-137, 2005.
DOI : 10.1007/11804192_6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.63.613

F. Bobot, Logique de séparation et vérification déductive, Thèse de doctorat, 2011.

F. Bobot, S. Conchon, E. Contejean, and M. Iguernelala, Stéphane Lescuyer, and Alain Mebsout. The Alt-Ergo automated theorem prover, 2008.

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

R. Burstall, Some techniques for proving correctness of programs which alter data structures, Machine Intelligence, vol.7, pp.23-50, 1972.

L. De, M. , and N. Bjørner, Z3, an efficient SMT solver, TACAS, pp.337-340, 2008.

L. De, M. , and B. Dutertre, Yices: An SMT Solver

J. Filliâtre, A. Paskevich, and A. Stump, The 2nd Verified Software Competition, 2011.

B. Jacobs and F. Piessens, The verifast program verifier, CW Reports, vol.520, 2008.

B. Jacobs, J. Smans, and F. Piessens, Verifying the composite pattern using separation logic, Workshop on Specification and Verification of Component- Based Systems, Challenge Problem Track, 2008.

B. Jacobs, J. Smans, and F. Piessens, A Quick Tour of the VeriFast Program Verifier, Programming Languages and Systems (APLAS 2010), pp.304-311, 2010.
DOI : 10.1007/978-3-642-17164-2_21

T. Ioannis and . Kassios, Dynamic frames: Support for framing, dependencies and sharing without restrictions, 14th International Symposium on Formal Methods (FM'06), pp.268-283, 2006.

V. Klebanov, P. Müller, N. Shankar, G. T. Leavens, V. Wüstholz et al., The 1st Verified Software Competition: Experience Report, Proceedings, 17th International Symposium on Formal Methods, 2011.
DOI : 10.1007/978-3-540-71067-7_6

K. Shuvendu, S. Lahiri, D. Qadeer, and . Walker, Linear maps, Proceedings of the 5th ACM workshop on Programming languages meets program verification, pp.3-14, 2011.

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

K. Rustan and M. Leino, VACID-0: Verification of ample correctness of invariants of data-structures, edition 0, Proceedings of Tools and Experiments Workshop at VSTTE, 2010.

Y. Moy and C. Marché, The Jessie plugin for Deduction Verification in Frama-C ? Tutorial and Reference Manual, INRIA & LRI, 2011.

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

S. Rosenberg, A. Banerjee, and D. A. Naumann, Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients, Lecture Notes in Computer Science, vol.6217, pp.183-198, 2010.
DOI : 10.1007/978-3-642-15057-9_13

J. Smans, B. Jacobs, and F. Piessens, Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic, ECOOP 2009 ? Object-Oriented Programming, pp.148-172, 2009.
DOI : 10.1007/978-3-540-78163-9_19

A. J. Summers and S. Drossopoulou, Considerate Reasoning and the Composite Design Pattern, Lecture Notes in Computer Science, vol.5944, pp.328-344, 2010.
DOI : 10.1007/978-3-642-11319-2_24