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
VACID-0: Verification of ample correctness of invariants of data-structures, edition 0, Proceedings of Tools and Experiments Workshop at VSTTE, 2010. ,
An algorithm for the organization of information, Soviet Mathematics?Doklady, vol.3, issue.5, pp.1259-1263, 1962. ,
Finger trees: a simple general-purpose data structure, Journal of Functional Programming, vol.16, issue.02, pp.197-217, 2006. ,
DOI : 10.1017/S0956796805005769
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
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
AVL Trees Archive of Formal Proofs, 2004. ,
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
Efficient Verified Red-Black Trees, 2011. ,
Program Verification Through Characteristic Formulae, Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming. ICFP '10, pp.321-332, 2010. ,
The Isabelle Collections Framework, Lecture Notes in Computer Science, vol.6172, pp.339-354, 2010. ,
DOI : 10.1007/978-3-642-14052-5_24
Program-ing finger trees in Coq, 12th ACM SIGPLAN International Conference on Functional Programming, pp.13-24, 2007. ,
Finger Trees Archive of Formal Proofs, 2010. ,