G. T. Leavens, K. R. Leino, and P. Müller, Specification and verification challenges for sequential object-oriented programs, Formal Aspects of Computing, vol.23, issue.9, pp.159-189, 2007.
DOI : 10.1007/s00165-007-0026-7

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.

G. M. Adel-'son-vel-'ski?-i and E. M. Landis, An algorithm for the organization of information, Soviet Mathematics?Doklady, vol.3, issue.5, pp.1259-1263, 1962.

R. Hinze and R. Paterson, Finger trees: a simple general-purpose data structure, Journal of Functional Programming, vol.16, issue.02, pp.197-217, 2006.
DOI : 10.1017/S0956796805005769

F. Bobot, J. C. Filliâtre, C. Marché, and A. Paskevich, Why3: Shepherd your herd of provers, Boogie 2011: First International Workshop on Intermediate Verification Languages, pp.53-64, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

J. C. Filliâtre and P. Letouzey, Functors for Proofs and Programs, Proceedings of The European Symposium on Programming, pp.370-384, 2004.
DOI : 10.1007/978-3-540-24725-8_26

T. Nipkow and C. Pusch, AVL Trees Archive of Formal Proofs, 2004.

R. Ralston, ACL2-certified AVL trees, Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 '09, pp.71-74, 2009.
DOI : 10.1145/1637837.1637848

A. Appel, Efficient Verified Red-Black Trees, 2011.

A. Charguéraud, Program Verification Through Characteristic Formulae, Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming. ICFP '10, pp.321-332, 2010.

P. Lammich and A. Lochbihler, The Isabelle Collections Framework, Lecture Notes in Computer Science, vol.6172, pp.339-354, 2010.
DOI : 10.1007/978-3-642-14052-5_24

M. Sozeau, Program-ing finger trees in Coq, 12th ACM SIGPLAN International Conference on Functional Programming, pp.13-24, 2007.

B. Nordhoff, S. Körner, and P. Lammich, Finger Trees Archive of Formal Proofs, 2010.