F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Let???s verify this with Why3, International Journal on Software Tools for Technology Transfer, vol.7, issue.5, p.709727, 2015.
DOI : 10.1007/s10009-014-0314-5

M. Clochard, J. Filliâtre, C. Marché, and A. Paskevich, Formalizing semantics with an automatic program verier, 6th Working Conference on Veried Software : Theories, Tools and Experiments (VSTTE), p.3751, 2014.

C. Dross, J. Filliâtre, and Y. Moy, Correct Code Containing Containers, 5th International Conference on Tests and Proofs, p.102118, 2011.
DOI : 10.1145/1375581.1375624
URL : https://hal.archives-ouvertes.fr/hal-00777683

J. Filliâtre, Backtracking iterators, Proceedings of the 2006 workshop on ML , ML '06, 2006.
DOI : 10.1145/1159876.1159885

J. Filliâtre, Deductive software verication, International Journal on Software Tools for Technology Transfer (STTT), vol.13, issue.5, p.397403, 2011.

J. Filliâtre, One Logic to Use Them All, 24th International Conference on Automated Deduction, 2013.
DOI : 10.1007/978-3-642-38574-2_1

J. Filliâtre, L. Gondelman, and A. Paskevich, The spirit of ghost code, 26th International Conference on Computer Aided Verication, p.116, 2014.

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, p.125128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

G. Huet, The Zipper, Journal of Functional Programming, vol.7, issue.5, p.549554, 1997.
DOI : 10.1017/S0956796897002864

G. Kulczycki, M. Sitaraman, J. Krone, J. E. Hollingsworth, W. F. Ogden et al., A language for building veried software components, Safe and Secure Software Reuse -13th International Conference on Software Reuse, ICSR 2013 Proceedings, volume 7925 of Lecture Notes in Computer Science, p.308314, 2013.

K. Rustan, M. Leino, and R. Monahan, Dafny meets the verication benchmarks challenge, Veried Software : Theories, Tools, Experiments, Third International Conference Proceedings, volume 6217 of Lecture Notes in Computer Science, p.112126, 2010.

K. Rustan, M. Leino, and W. Schulte, Using history invariants to verify observers, Lecture Notes in Computer Science, vol.4421, p.8094, 2007.

N. Polikarpova, J. Tschannen, and C. A. Furia, A fully veried container library, FM 2015 : Formal Methods -20th International Symposium Proceedings, volume 9109 of Lecture Notes in Computer Science, p.414434, 2015.

W. Bruce and . Weide, Savcbs 2006 challenge : Specication of iterators, Proceedings of the 2006 Conference on Specication and Verication of Component-based Systems, SAVCBS '06, p.7577, 2006.