J. Barnes, Programming in Ada 2012, 2014.
DOI : 10.1017/CBO9781139696616

M. Barnett, R. Deline, B. Jacobs, B. Y. Chang, and K. R. Leino, Boogie: A Modular Reusable Verifier for Object-Oriented Programs, FMCO. LNCS, pp.364-387, 2005.
DOI : 10.1007/11804192_17

C. W. Barrett, D. L. Dill, and J. R. Levitt, A decision procedure for bit-vector arithmetic, Proceedings of the 35th annual conference on Design automation conference , DAC '98, pp.522-527, 1998.
DOI : 10.1145/277044.277186

G. Berry, The foundations of Esterel In: Proof, Language, and Interaction, Essays in Honour of Robin Milner, pp.425-454, 2000.

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

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

S. Boldo and C. Marché, Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs, Mathematics in Computer Science, vol.1, issue.2, pp.377-393, 2011.
DOI : 10.1007/s11786-011-0099-9
URL : https://hal.archives-ouvertes.fr/hal-00777605

M. Brain, C. Tinelli, P. Ruemmer, and T. Wahl, An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic, 2015 IEEE 22nd Symposium on Computer Arithmetic, pp.160-167, 2015.
DOI : 10.1109/ARITH.2015.26

R. E. Bryant, D. Kroening, J. Ouaknine, S. A. Seshia, O. Strichman et al., An abstraction-based decision procedure for bit-vector arithmetic, International Journal on Software Tools for Technology Transfer, vol.11, issue.2, pp.95-104, 2009.
DOI : 10.1007/s10009-009-0101-x

R. Chapman and F. Schanda, Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK, ITP. LNCS, pp.17-26, 2014.
DOI : 10.1007/978-3-319-08970-6_2

D. Cyrluk, H. Rueß, and O. Möller, An efficient decision procedure for the theory of fixed-sized bit-vectors, Computer Aided Verification, pp.60-71, 1997.
DOI : 10.1007/3-540-63166-6_9

M. Dahlweid, M. Moskal, T. Santen, S. Tobies, and W. Schulte, VCC: Contract-based modular verification of concurrent C, 2009 31st International Conference on Software Engineering, Companion Volume, pp.429-430, 2009.
DOI : 10.1109/ICSE-COMPANION.2009.5071046

C. Dross, C. Fumex, J. Gerlach, and C. Marché, High-level functional properties of bit-level programs: Formal specifications and automated proofs, Research Report Inria, vol.8821, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01238376

J. C. Filliâtre, Verifying Two Lines of C with Why3: An Exercise in Program Verification, VSTTE. LNCS, pp.83-97, 2012.
DOI : 10.1145/360051.360224

J. Gerlach, Validation and verification of implementation/code, OpenETCS, 2015.

J. Kanig, E. Schonberg, and C. Dross, Hi-Lite, Proceedings of the 2012 ACM conference on High integrity language technology, HILT '12, pp.27-34, 2012.
DOI : 10.1145/2402676.2402690

K. R. Leino and V. Wüstholz, The Dafny Integrated Development Environment, Electronic Proceedings in Theoretical Computer Science, vol.149, pp.3-15, 2014.
DOI : 10.4204/EPTCS.149.2

C. Lomont, Fast inverse square root, Tech. rep, 2003.

J. W. Mccormick and P. C. Chapin, Building High Integrity Applications with SPARK, 2015.
DOI : 10.1017/CBO9781139629294

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

T. M. Nguyen, Taking architecture and compiler into account in formal proofs of numerical programs, Thèse de doctorat, 2012.
URL : https://hal.archives-ouvertes.fr/tel-00710193

H. S. Warren, Hackers's Delight, 2003.