F. Bobot, J. C. 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, pp.709-727, 2015.
DOI : 10.1007/s10009-014-0314-5

R. S. Boyer and J. S. Moore, MJRTY???A Fast Majority Vote Algorithm, Automated Reasoning: Essays in Honor of Woody Bledsoe, pp.105-118, 1991.
DOI : 10.1007/978-94-011-3488-0_5

A. Charguéraud, Characteristic formulae for the verification of imperative programs, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming (ICFP), pp.418-430, 2011.

M. Clochard, J. C. Filliâtre, C. Marché, and A. Paskevich, Formalizing Semantics with an Automatic Program Verifier, 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), pp.37-51, 2014.
DOI : 10.1007/978-3-319-12154-3_3
URL : https://hal.archives-ouvertes.fr/hal-01067197

J. O. Coplien, Advanced C++ Programming Styles and Idioms, Proceedings. Technology of Object-Oriented Languages and Systems, TOOLS 25 (Cat. No.97TB100239), 1992.
DOI : 10.1109/TOOLS.1997.681881

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

J. C. Filliâtre, One logic to use them allCADE-24), 24th International Conference on Automated Deduction, pp.1-20, 2013.

J. C. Filliâtre, L. Gondelman, and A. Paskevich, The spirit of ghost code, 26th International Conference on Computer Aided Verification, pp.1-16, 2014.

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

G. Kulczycki, M. Sitaraman, J. Krone, J. E. Hollingsworth, W. F. Ogden et al., A Language for Building Verified Software Components, Safe and Secure Software Reuse. ICSR 2013, pp.308-314, 2013.
DOI : 10.1007/978-3-642-38977-1_23

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal, Ynot: Reasoning with the awkward squad, Proceedings of ICFP'08, 2008.

N. Polikarpova, J. Tschannen, and C. A. Furia, A Fully Verified Container Library, LNCS, vol.2015, issue.9109, pp.414-434, 2015.
DOI : 10.1007/978-3-319-19249-9_26

P. M. Rondon, M. Kawaguchi, and R. Jhala, Liquid types, pp.159-169, 2008.

N. Swamy, C. Hri?cu, C. Keller, A. Rastogi, A. Delignat-lavaud et al., Dependent types and multi-monadic effects in F*, 43rd ACM Symposium on Principles of Programming Languages (POPL). pp, pp.256-270
URL : https://hal.archives-ouvertes.fr/hal-01265793

N. Vazou, P. Rondon, and R. Jhala, Abstract Refinement Types, Programming Languages and Systems, pp.209-228, 2013.
DOI : 10.1007/978-3-642-37036-6_13

B. W. Weide, SAVCBS 2006 challenge, Proceedings of the 2006 conference on Specification and verification of component-based systems , SAVCBS '06, 2006.
DOI : 10.1145/1181195.1181211