Multi-Prover Verification of Floating-Point Programs, In: Int. Joint Conference on Automated Reasoning. LNAI, vol.6173, pp.127-141, 2010. ,
DOI : 10.1007/978-3-642-14203-1_11
URL : https://hal.archives-ouvertes.fr/inria-00534333
CodePeer ? beyond bug-finding with static analysis, Static Analysis of Software: the Abstract Interpretation, 2013. ,
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
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program, Journal of Automated Reasoning, vol.200, issue.25???28, pp.423-456, 2013. ,
DOI : 10.1007/s10817-012-9255-4
URL : https://hal.archives-ouvertes.fr/hal-00649240
Formal Verification of Floating-Point Programs, 18th IEEE Symposium on Computer Arithmetic (ARITH '07), pp.187-194, 2007. ,
DOI : 10.1109/ARITH.2007.20
URL : https://hal.archives-ouvertes.fr/hal-01174892
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
Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq, 2011 IEEE 20th Symposium on Computer Arithmetic, pp.243-252, 2011. ,
DOI : 10.1109/ARITH.2011.40
URL : https://hal.archives-ouvertes.fr/inria-00534854
Deciding floating-point logic with abstract conflict driven clause learning, Formal Methods in System Design, vol.48, issue.5, pp.213-245, 2014. ,
DOI : 10.1007/s10703-013-0203-7
Specification of the IEEE-854 floating-point standard in HOL and PVS, Int. Workshop on Higher-Order Logic Theorem Proving and Its Applications, 1995. ,
Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK, Interactive Theorem Proving, pp.17-26, 2014. ,
DOI : 10.1007/978-3-319-08970-6_2
Sharpening Constraint Programming Approaches for Bit-Vector Theory, p.CPAIOR, 2017. ,
DOI : 10.1109/DATE.2001.915055
A three-tier strategy for reasoning about floating-point numbers in SMT, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01522770
Frama-C, Int. Conf. on Software Engineering and Formal Methods, pp.233-247, 2012. ,
DOI : 10.1007/978-3-642-33826-7_16
Certification of bounds on expressions involving rounded operators, ACM Transactions on Mathematical Software, vol.37, issue.1, pp.1-20, 2010. ,
DOI : 10.1145/1644001.1644003
URL : https://hal.archives-ouvertes.fr/hal-00127769
A Generic Library for Floating-Point Numbers and Its Application to Exact Computing, Theorem Proving in Higher Order Logics, pp.169-184, 2001. ,
DOI : 10.1007/3-540-44755-5_13
URL : https://hal.archives-ouvertes.fr/hal-00157285
Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software, FMICS. LNCS, pp.53-69, 2009. ,
DOI : 10.1007/978-3-642-04570-7_6
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, Computer Aided Verification, pp.173-177, 2007. ,
DOI : 10.1007/978-3-540-73368-3_21
Specification and proof of highlevel functional properties of bit-level programs, 8th NASA Formal Methods Symposium, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01314876
Automated verification of floating-point computations in Ada programs, Inria, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01511183
Verification of Numerical Programs: From Real Numbers to Floating Point Numbers, NASA Formal Methods, pp.441-446, 2013. ,
DOI : 10.1007/978-3-642-38088-4_31
Floating point verification in HOL light: The exponential function, Formal Methods in System Design, vol.16, issue.3, pp.271-305, 2000. ,
DOI : 10.1007/BFb0000475
Formal Verification of Floating Point Trigonometric Functions, LNCS, vol.1954, pp.217-233, 2000. ,
DOI : 10.1007/3-540-40922-X_14
Floating-point verification, Int. Symp. of Formal Methods Europe, pp.529-532, 2005. ,
DOI : 10.1007/11526841_35
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.1549
Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014, Int. Symp. on Leveraging Applications of Formal Methods, Verification and Validation, pp.461-478, 2016. ,
DOI : 10.1007/978-3-662-46681-0_53
URL : https://hal.archives-ouvertes.fr/hal-01344110
Usable auto-active verification, 2010. ,
Verification of the functional behavior of a floating-point program: An industrial case study, Science of Computer Programming, vol.96, issue.3, pp.279-296, 2014. ,
DOI : 10.1016/j.scico.2014.04.003
Improving the Floating Point Addition and Subtraction Constraints, Principles and Practice of Constraint Programming, pp.360-367, 2010. ,
DOI : 10.1007/978-3-642-15396-9_30
Building High Integrity Applications with SPARK, 2015. ,
DOI : 10.1017/CBO9781139629294
Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors, European Symposium on Programming, pp.3-17, 2004. ,
DOI : 10.1007/978-3-540-24725-8_2
The pitfalls of verifying floating-point computations, ACM Transactions on Programming Languages and Systems, vol.30, issue.3, p.12, 2008. ,
DOI : 10.1145/1353445.1353446
URL : https://hal.archives-ouvertes.fr/hal-00128124
Z3: An Efficient SMT Solver, LNCS, vol.4963, pp.337-340, 2008. ,
DOI : 10.1007/978-3-540-78800-3_24
An SMT-LIB theory of binary floating-point arithmetic, In: Int. Workshop on Satisfiability Modulo Theories, 2010. ,
Abstract, LMS Journal of Computation and Mathematics, vol.11, pp.148-200, 1998. ,
DOI : 10.1112/S1461157000000176