B. Aydemir, A. Bohannon, M. Fairbairn, J. Foster, B. Pierce et al., Mechanized Metatheory for the Masses: The PoplMark Challenge, Proceedings of the Eighteenth International Conference on Theorem Proving in Higher Order Logics number 3603 in Lecture Notes in Computer Science, pp.50-65, 2005.
DOI : 10.1007/11541868_4

R. Back and J. Wright, Refinement calculus -a systematic introduction. Undergraduate texts in computer science, 1999.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

F. Bobot, S. Conchon, E. Contejean, M. Iguernelala, S. Lescuyer et al., The Alt-Ergo automated theorem prover, 2008.

F. Bobot, J. Filliâtre, C. Marché, G. Melquiond, and A. Paskevich, The Why3 platform, version 0.80. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0, 2012.

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, pp.53-64, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

S. Conchon and J. Filliâtre, Semi-persistent Data Structures, 17th European Symposium on Programming (ESOP'08), 2008.
DOI : 10.1007/978-3-540-78739-6_25

L. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

P. Herms, C. Marché, and B. Monate, A Certified Multi-prover Verification Condition Generator, Verified Software : Theories, Tools, Experiments (4th International Conference VSTTE), pp.2-17, 2012.
DOI : 10.1007/3-540-48118-4_45
URL : https://hal.archives-ouvertes.fr/hal-00639977

C. Marché and A. Tafat, Weakest precondition calculus, revisited using Why3, 2012.

S. Schulz, System Description: E??0.81, Second International Joint Conference on Automated Reasoning, pp.223-228, 2004.
DOI : 10.1007/978-3-540-25984-8_15

C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda et al., SPASS Version 3.5, 22nd International Conference on Automated Deduction, pp.140-145, 2009.
DOI : 10.1007/978-3-540-73595-3_38