. Bitspec, MaxValue at bitspec.ads:13 flow analyzed (0 errors and 0 warnings) and proved (0 checks

. Bitspec, Nth8 _ Stream at bitspec.ads:9 flow analyzed (0 errors and 0 warnings) and proved (5 checks) in unit bittypes, 1 subprograms and packages out of 1 analyzed BitTypes at bittypes.ads:3 flow analyzed (0 errors and 0 warnings) and proved (0 checks) in unit bitwalker, 12 subprograms and packages out of 12 analyzed Bitwalker at bitwalker.ads:6 flow analyzed

. Bitwalker, LemmaFunction at bitwalker.ads:119 flow analyzed (0 errors and 0 warnings) and proved (18 checks) Bitwalker.Peek at bitwalker.ads:36 flow analyzed (0 errors and 0 warnings) and proved

. Bitwalker, PeekBit64 at bitwalker.ads:55 flow analyzed (0 errors and 0 warnings) and proved

. Bitwalker, PeekBit8 at bitwalker.ads:9 flow analyzed (0 errors and 0 warnings) and proved

. Bitwalker, PeekBit8Array at bitwalker.ads:15 flow analyzed (0 errors and 0 warnings) and proved

. Bitwalker, PeekThenPoke at bitwalker.ads:127 flow analyzed (0 errors and 0 warnings) and proved (12 checks) Bitwalker.Poke at bitwalker.ads:88 flow analyzed (0 errors and 0 warnings) and proved

. Bitwalker, PokeBit64 at bitwalker.ads:23 flow analyzed (0 errors and 0 warnings) and proved

. Bitwalker, PokeBit8 at bitwalker.ads:64 flow analyzed (0 errors and 0 warnings) and proved

. Bitwalker, PokeBit8Array at bitwalker.ads:76 flow analyzed (0 errors and 0 warnings) and proved

. Bitwalker, PokeThenPeek at bitwalker.ads:142 flow analyzed (0 errors and 0 warnings) and proved (9 checks) in unit testwalker, 0 subprograms and packages out of 1 analyzed Testwalker at testwalker.adb:7 skipped Inria References [1] John Barnes, Programming in Ada 2012, 2014.

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

P. Baudin, J. Filliâtre, C. Marché, B. Monate, Y. Moy et al., ACSL: ANSI/ISO C Specification Language, version 1, 2009.

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

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

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, 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

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, Interactive Theorem Proving -5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 Proceedings, volume 8558 of Lecture Notes in Computer Science, pp.17-26, 2014.
DOI : 10.1007/978-3-319-08970-6_2

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles et al., Frama-C, Proceedings of the 10th International Conference on Software Engineering and Formal Methods, number 7504 in Lecture Notes in Computer Science, pp.233-247, 2012.
DOI : 10.1007/978-3-642-33826-7_16

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

L. De, M. , and N. Bjørner, Z3, an efficient SMT solver, TACAS, pp.337-340, 2008.

J. Filliâtre, Verifying Two Lines of C with Why3: An Exercise in Program Verification, Verified Software: Theories, Tools, Experiments (4th International Conference VSTTE), pp.83-97, 2012.
DOI : 10.1145/360051.360224

J. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, 19th International Conference on Computer Aided Verification, pp.173-177, 2007.
DOI : 10.1007/978-3-540-73368-3_21

J. 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

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
DOI : 10.1145/2402676.2402690

V. Klebanov, P. Müller, N. Shankar, G. T. Leavens, V. Wüstholz et al., The 1st Verified Software Competition: Experience Report, Proceedings , 17th International Symposium on Formal Methods, 2011.
DOI : 10.1007/978-3-540-71067-7_6

K. Rustan, M. Leino, and V. Wüstholz, The dafny integrated development environment, Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014 of Electronic Proceedings in Theoretical Computer Science, pp.3-15, 2014.

C. Lomont, Fast inverse square root, 2003.

W. John, P. C. Mccormick, and . Chapin, Building High Integrity Applications with SPARK, 2015.

T. M. and T. 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

P. Rümmer and T. Wahl, An smt-lib theory of binary floating-point arithmetic, Informal proceedings of 8th International Workshop on Satisfiability Modulo Theories (SMT) at FLoC, 2010.

S. Henry and . Warren, Hackers's Delight, 2003.