Formal verification of iterative algorithms in microprocessors, Proceedings Design Automation Conference (DAC 2000), pp.201-206, 2000. ,
The B-book: assigning programs to meanings, 1996. ,
Weakest-precondition of Unstructured Programs, SIGSOFT Softw. Eng. Notes, vol.31, issue.1, pp.82-87, 2005. ,
, CAV'11), vol.6806, pp.171-177, 2011.
, The SMT-LIB, 2010.
A Proof of GMP Square Root, Journal of Automated Reasoning, vol.29, issue.3-4, pp.225-252, 2002. ,
URL : https://hal.archives-ouvertes.fr/inria-00101044
Industrial Experience with SPARK, Ada Letters XX, issue.4, 2000. ,
Alt-Ergo 2.2, SMT Workshop: International Workshop on SMT, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01960203
Z3: An Efficient SMT Solver, 2008. ,
Guarded Commands, Nondeterminacy and Formal Derivation of Programs, ACM, vol.18, issue.8, pp.453-457, 1975. ,
Computer Aided Verification. 737-744, 2014. ,
Digit Serial Methods with Applications to Division and Square Root, IEEE Transactions on Computers, vol.67, issue.3, pp.449-456, 2018. ,
Avoiding Exponential Explosion: Generating Compact Verification Conditions, SIGPLAN Not, vol.36, issue.3, pp.193-205, 2001. ,
Formal Verification of Square Root Algorithms, Formal Methods in System Design, vol.22, issue.2, pp.143-153, 2003. ,
An Axiomatic Basis for Computer Programming, 1969. ,
Frama-C: A software analysis perspective, Formal Aspects of Computing, vol.27, issue.3, 2015. ,
URL : https://hal.archives-ouvertes.fr/cea-01808981
Standardization and testing of implementations of mathematical functions in floating point numbers, Programming and Computer Software, vol.33, issue.3, pp.154-173, 2007. ,
Astrée: Verification of Absence of Runtime Error, Building the Information Society: IFIP 18th World Computer Congress Topical Sessions 22-27, pp.385-392, 2004. ,
Formal Verification of a State-of-the-Art Integer Square Root, IEEE 26th Symposium on Computer Arithmetic (ARITH), pp.183-186, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02092970
Testing or Formal Verification: DO-178C Alternatives and Industrial Experience, IEEE Soft, vol.30, issue.3, 2013. ,
Formal verification of division and square root implementations, an Oracle report, 16th Conference on Formal Methods in Computer-Aided Design, pp.149-152, 2016. ,
Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems, 1999. ,
A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode, Formal Methods in System Design, vol.14, issue.1, pp.75-125, 1999. ,
A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division, and Square Root Algorithm of the AMDK7 Processor, J. Comput. Math. (UK), vol.1, 1998. ,
Mechanical Verification of a Square Root Algorithm Using Taylor's Theorem, Lecture Notes in Computer Science, vol.2517, pp.274-291, 2002. ,
Verification and synthesis of addition programs under the rules of correctness of statements, Automatic Control and Computer Sciences, vol.45, issue.7, pp.421-427, 2011. ,
Generation of correctness conditions for imperative programs, Programming and Computer Software, vol.34, issue.6, pp.307-321, 2008. ,
Platform-independent Specification and Verification of the Standard Mathematical Square Root Function. Modeling and Analysis of, Information Systems, vol.25, issue.6, pp.637-666, 2018. ,
Formal Verification of Automotive Embedded Software, Proceedings of the 6th Conference on Formal Methods in Software Engineering, vol.18, pp.84-87, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01768687