, Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL, The Computer Journal, vol.53, issue.4, pp.465-488, 2010.
DOI : 10.1093/comjnl/bxp023
, Verifying Object-Oriented Programs with KeY: A??Tutorial, Formal Methods for Components and Objects, pp.70-101, 2007.
DOI : 10.1007/978-3-540-74792-5_4
, The B-book: assigning programs to meanings, 2005.
DOI : 10.1017/CBO9780511624162
, The algorithmic analysis of hybrid systems, Theoretical Computer Science, vol.138, issue.1, pp.3-34, 1995.
DOI : 10.1016/0304-3975(94)00202-T
, Formal Verification of Backward Compatibility of Microcode, Computer Aided Verification, pp.185-198, 2005.
DOI : 10.1007/11513988_20
, On construction of a library of formally verified low-level arithmetic functions, Innovations in Systems and Software Engineering, pp.59-77, 2013.
, Multi-Prover Verification of Floating-Point Programs, Fifth International Joint Conference on Automated Reasoning, pp.127-141, 2010.
DOI : 10.1007/978-3-642-14203-1_11
URL : https://hal.archives-ouvertes.fr/inria-00534333
, The formal verification of a pipelined double-precision IEEE floating-point multiplier, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, pp.7-10, 1995.
, Formal methods applied to a floating-point number system, IEEE Transactions on Software Engineering, vol.15, issue.5, pp.611-621, 1989.
DOI : 10.1109/32.24710
, Non-standard semantics of hybrid systems modelers, Journal of Computer and System Sciences, vol.78, issue.3, pp.877-910, 2012.
DOI : 10.1016/j.jcss.2011.08.009
URL : https://hal.archives-ouvertes.fr/hal-00766726
, Interactive Theorem Proving and Program Development. Coq'Art : the Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237
, An overview of JML tools and applications, International Journal on Software Tools for Technology Transfer, vol.box, issue.3, pp.212-232, 2005.
DOI : 10.1007/s10009-004-0167-4
, Formal Proof of a Wave Equation Resolution Scheme: The Method Error, Proceedings of the first Interactive Theorem Proving Conference (ITP), pp.147-162, 2010.
DOI : 10.1007/978-3-642-14052-5_12
URL : https://hal.archives-ouvertes.fr/inria-00450789
, 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
, ACSL: ANSI/ISO C Specification Language, version 1, 2014.
, Trusting computations: A mechanized proof from partial differential equations to actual program, Computers & Mathematics with Applications, vol.68, issue.3, pp.325-352, 2014.
DOI : 10.1016/j.camwa.2014.06.004
URL : https://hal.archives-ouvertes.fr/hal-00769201
, A mechanically-validated technique for extending the available precision, Conference Record of Thirty-Fifth Asilomar Conference on Signals, Systems and Computers (Cat.No.01CH37256), pp.1299-1303, 2001.
DOI : 10.1109/ACSSC.2001.987700
, Properties of the subtraction valid for any floating point system, 7th International Workshop on Formal Methods for Industrial Critical Systems, pp.137-149, 2002.
DOI : 10.1016/S1571-0661(04)80408-0
URL : https://hal.archives-ouvertes.fr/inria-00072115
, Representable correcting terms for possibly underflowing floating point operations, 16th IEEE Symposium on Computer Arithmetic, 2003. Proceedings., pp.79-86, 2003.
DOI : 10.1109/ARITH.2003.1207663
, Properties of two???s complement floating point notations, International Journal on Software Tools for Technology Transfer, vol.22, issue.2-3, pp.237-246, 2004.
DOI : 10.1112/S1461157000000176
, A Simple Test Qualifying the Accuracy of Horner'S Rule for Polynomials, Numerical Algorithms, vol.37, issue.1-4, pp.45-60, 2004.
DOI : 10.1023/B:NUMA.0000049487.98618.61
, Proof and certification for an accurate discriminant, 12th IMACS-GAMM International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, 2006.
, Formally Verified Argument Reduction with a Fused Multiply-Add, IEEE Transactions on Computers, vol.58, issue.8, pp.1139-1145, 2009.
DOI : 10.1109/TC.2008.216
URL : https://hal.archives-ouvertes.fr/hal-00168401
, 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
, Combining Coq and Gappa for Certifying Floating-Point Programs, 16th Calculemus Symposium, pp.59-74, 2009.
DOI : 10.1109/TC.2008.200
URL : https://hal.archives-ouvertes.fr/inria-00432726
, Preserving User Proofs across Specification Changes, Verified Software: Theories, Tools, Experiments (5th International Conference VSTTE), pp.191-201, 2013.
DOI : 10.1007/978-3-642-54108-7_10
URL : https://hal.archives-ouvertes.fr/hal-00875395
, Symbolic execution of floating-point computations. Software Testing, Verification and Reliability, pp.97-121, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00540299
, HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment, Proceedings of the 21st International Conference on Computer Aided Verification, CAV '09, pp.620-626, 2009.
DOI : 10.1007/978-3-642-02658-4_46
, A dynamic program analysis to find floating-point accuracy problems, PLDI '12: Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012.
, ARPREC: An arbitrary precision computation package, 2002.
DOI : 10.2172/817634
, Verification of objectoriented software: The KeY approach, 2007.
, A Formally-Verified C Compiler Supporting Floating-Point Arithmetic, 2013 IEEE 21st Symposium on Computer Arithmetic, pp.107-115, 2013.
DOI : 10.1109/ARITH.2013.30
URL : https://hal.archives-ouvertes.fr/hal-00743090
, Verified Compilation of Floating-Point Computations, Journal of Automated Reasoning, vol.1, issue.1, 2014.
DOI : 10.1007/s10817-014-9317-x
URL : https://hal.archives-ouvertes.fr/hal-00862689
, Rigorous Polynomial Approximation Using Taylor Models in Coq, In NASA Formal Methods, pp.85-99, 2012.
DOI : 10.1007/978-3-642-28891-3_9
URL : https://hal.archives-ouvertes.fr/ensl-00653460
, Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives, Proceedings of the The Second International Conference on Certified Programs and Proofs, pp.289-304, 2012.
DOI : 10.1007/978-3-642-35308-6_22
URL : https://hal.archives-ouvertes.fr/hal-00712938
, Coquelicot: A userfriendly library of real analysis for coq, Mathematics in Computer Science, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00860648
, Formalization of real analysis: a survey of proof assistants and libraries, Mathematical Structures in Computer Science, vol.11, issue.07, 2014.
DOI : 10.1007/3-540-44755-5_5
URL : https://hal.archives-ouvertes.fr/hal-00806920
, The Spec# Programming System: An Overview, Proceedings of the 2004 International Conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS'04, pp.49-69, 2005.
DOI : 10.1007/978-3-540-30569-9_3
, Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models, Reliable Computing, vol.4, issue.4, pp.361-369, 1998.
DOI : 10.1023/A:1024467732637
, Some functions computable with a fusedmac, Proceedings of the 17th Symposium on Computer Arithmetic, pp.52-58, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00000895
, Provably faithful evaluation of polynomials, Proceedings of the 2006 ACM symposium on Applied computing , SAC '06, pp.1328-1332, 2006.
DOI : 10.1145/1141277.1141586
URL : https://hal.archives-ouvertes.fr/inria-00000892
, Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd, IEEE Transactions on Computers, vol.57, issue.4, pp.462-471, 2008.
DOI : 10.1109/TC.2007.70819
URL : https://hal.archives-ouvertes.fr/inria-00080427
, 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
, Exact and Approximated Error of the FMA, IEEE Transactions on Computers, vol.60, issue.2, pp.157-164, 2011.
DOI : 10.1109/TC.2010.139
URL : https://hal.archives-ouvertes.fr/inria-00429617
, Long-term stability of the tevatron by verified global optimization. Nuclear Instruments and Methods in Physics Research Section A: Accelerators, Spectrometers, Detectors and Associated Equipment, pp.1-10, 2006.
, A proof of GMP square root, Journal of Automated Reasoning, vol.29, issue.3/4, pp.225-252, 2002.
DOI : 10.1023/A:1021987403425
URL : https://hal.archives-ouvertes.fr/inria-00101044
, Hardware-independent proofs of numerical programs, Proceedings of the Second NASA Formal Methods Symposium, number NASA/CP-2010-216215 in NASA Conference Publication, pp.14-23, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00534410
, Proofs of numerical programs when the compiler optimizes, Innovations in Systems and Software Engineering, pp.151-160, 2011.
DOI : 10.1007/s11334-011-0151-6
URL : https://hal.archives-ouvertes.fr/hal-00777639
, Bridging the gap between formal specification and bit-level floatingpoint arithmetic, Proceedings of the 6th Conference on Real Numbers and Computers, pp.22-36, 2004.
, Preuves formelles en arithmétiques à virgule flottante, 2004.
, Formal Proofs about DSPs, Algebraic and Numerical Algorithms and Computer-assisted Proofs, number 05391 in Dagstuhl Seminar Proceedings Internationales Begegnungs-und Forschungszentrum (IBFI), Schloss Dagstuhl, 2006.
, Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms, Proceedings of the third International Joint Conference on Automated Reasoning (IJCAR), pp.52-66, 2006.
DOI : 10.1007/11814771_6
, Floats and Ropes: A Case Study for Formal Numerical Program Verification, 36th International Colloquium on Automata, Languages and Programming, pp.91-102, 2009.
DOI : 10.1007/978-3-642-02930-1_8
, How to Compute the Area of a Triangle: A Formal Revisit, 2013 IEEE 21st Symposium on Computer Arithmetic, pp.91-98, 2013.
DOI : 10.1109/ARITH.2013.29
URL : https://hal.archives-ouvertes.fr/hal-00862653
, Analyse statique par interpretation abstraite de systèmes hybrides, 2008.
, Proving the correctness of the implementation of a controlcommand algorithm, Static Analysis Symposium, pp.102-119, 2009.
, Automatic detection of floating-point exceptions, Proceedings of the 40th annual ACM SIGPLAN- SIGACT symposium on Principles of programming languages, pp.549-560, 2013.
, Interpretation of IEEE-854 floating-point standard and definition in the HOL system, 1995.
, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/hal-01108790
, Antoine Miné, David Monniaux, and Xavier Rival. The ASTRÉE analyzer, Programming Languages and Systems, pp.21-30, 2005.
, CC(X): Semantic Combination of Congruence Closure with Solvable Theories, Post-proceedings of the 5th International Workshop on Satisfiability Modulo Theories, pp.51-69, 2007.
DOI : 10.1016/j.entcs.2008.04.080
, VCC: A Practical System for Verifying Concurrent C, Proceedings of the 22Nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs '09, pp.23-42, 2009.
DOI : 10.1007/978-3-540-74591-4_15
, Efficient search for inputs causing high floating-point errors, Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), pp.43-52, 2014.
, Verifying the SRT division algorithm using theorem proving techniques. Formal Methods in System Design, pp.7-44, 1999.
, Efficient and accurate computation of upper bounds of approximation errors, Theoretical Computer Science, vol.412, issue.16, pp.1523-1543, 2011.
DOI : 10.1016/j.tcs.2010.11.052
URL : https://hal.archives-ouvertes.fr/ensl-00445343
, Specification of the IEEE-854 floatingpoint standard in HOL and PVS, International Workshop on Higher Order Logic Theorem Proving and its Applications, 1995.
, Abstract Simulation: A Static Analysis of Simulink Models, 2009 International Conference on Embedded Software and Systems, pp.83-92, 2009.
DOI : 10.1109/ICESS.2009.80
URL : https://hal.archives-ouvertes.fr/hal-00332447
, Built-in treatment of an axiomatic floating-point theory for SMT solvers, Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, pp.12-21, 2012.
, Inside the Pentium FDIV bug. Dr. Dobb's, Journal, vol.20, issue.148, pp.129-135, 1995.
, SMT Techniques and their Applications: from Alt-Ergo to Cubicle, 2012.
, Fidelity in mathematical discourse: Is one and one really two? The American Mathematical Monthly, pp.252-263, 1972.
, Correctly rounded exponential function in double-precision arithmetic, International Symposium on Optical Science and Technology International Society for Optics and Photonics, pp.156-167, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00072387
, Certifying the Floating-Point Implementation of an Elementary Function Using Gappa, IEEE Transactions on Computers, vol.60, issue.2, pp.242-253, 2011.
DOI : 10.1109/TC.2010.128
, A floating point technique for extending the available precision, Numerische Mathematik, vol.18, issue.3, pp.224-242, 1971.
, Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software, Formal Methods for Industrial Critical Systems, pp.53-69, 2009.
DOI : 10.1007/978-3-642-04570-7_6
, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, vol.18, issue.8, pp.453-457, 1975.
, Trustworthy numerical computation in Scala, Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp.325-344, 2011.
, Sound compilation of reals, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pp.235-248, 2014.
DOI : 10.1145/2535838.2535874
, Social processes and proofs of theorems and programs, Proceedings of the 4th ACM SIGACT- SIGPLAN symposium on Principles of programming languages, pp.206-214
, Certification of bounds on expressions involving rounded operators, TACAS, pp.1-20, 2008.
DOI : 10.1145/1644001.1644003
URL : https://hal.archives-ouvertes.fr/hal-00127769
, Provably Safe Coordinated Strategy for Distributed Conflict Resolution, AIAA Guidance, Navigation, and Control Conference and Exhibit, pp.2005-6047, 2005.
DOI : 10.2514/6.2005-6047
, A generic library of floatingpoint numbers and its application to exact computing, 14th International Conference on Theorem Proving in Higher Order Logics, pp.169-184, 2001.
, Using Computation to Decode the First Known Computer, Computer, vol.44, issue.7, pp.32-39, 2011.
DOI : 10.1109/MC.2011.134
, The spirit of ghost code, 26th International Conference on Computer Aided Verification, 2014.
, MPFR: A multiple-precision binary floating-point library with correct rounding, ACM Transactions on Mathematical Software, vol.33, issue.2, 2007.
, Verification of non-functional programs using interpretations in type theory, Journal of functional Programming, vol.13, issue.4, pp.709-745, 2003.
DOI : 10.1017/S095679680200446X
, Deductive Program Verification, 2011.
, One Logic to Use Them All, 24th International Conference on Automated Deduction (CADE-24), volume 7898 of LNAI, pp.1-20, 2013.
DOI : 10.1007/978-3-642-38574-2_1
, Multi-prover Verification of C Programs, 6th International Conference on Formal Engineering Methods, pp.15-29, 2004.
DOI : 10.1007/978-3-540-30482-1_10
, 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
, PHAVer: algorithmic verification of hybrid systems past HyTech, International Journal on Software Tools for Technology Transfer, vol.11, issue.2, pp.263-279, 2008.
DOI : 10.1007/s10009-007-0062-x
, More on algorithms that reveal properties of floating point arithmetic units, Communications of the ACM, vol.17, issue.5, pp.276-277, 1974.
DOI : 10.1145/360980.361003
, Introduction to HOL: a theorem proving environment for higher order logic, 1993.
, What every computer scientist should know about floating-point arithmetic, ACM Computing Surveys, vol.23, issue.1, pp.5-47, 1991.
DOI : 10.1145/103162.103163
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.7712
, From LCF to HOL: a short history, Proof, Language, and Interaction: Essays in Honor of Robin Milner, pp.169-186, 2000.
, Static Analysis of Numerical Algorithms, Static Analysis, pp.18-34, 2006.
DOI : 10.1007/11823230_3
, Robustness Analysis of Finite Precision Implementations, Programming Languages and SystemsGPV12] Eric Goubault, Sylvie Putot, and Franck Védrine. Modular static analysis with zonotopes Static Analysis, pp.50-57, 2012.
DOI : 10.1007/978-3-319-03542-0_4
, Verifying the accuracy of polynomial approximations in HOL, Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, pp.137-152, 1997.
DOI : 10.1007/BFb0028391
, A Machine-Checked Theory of Floating Point Arithmetic, 12th International Conference on Theorem Proving in Higher Order Logics, pp.113-130, 1999.
DOI : 10.1007/3-540-48256-3_9
, Floating point verification in HOL light: The exponential function . Formal Methods in System Design, pp.271-305, 2000.
, Formal Verification of Floating Point Trigonometric Functions, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, pp.217-233, 2000.
DOI : 10.1007/3-540-40922-X_14
, Overview, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, pp.60-66, 2009.
DOI : 10.1007/978-1-4302-0821-1_1
URL : https://hal.archives-ouvertes.fr/in2p3-00803620
, The HOL Light Theory of Euclidean Space, Journal of Automated Reasoning, vol.4, issue.2, pp.173-190, 2013.
DOI : 10.1007/s10817-012-9250-9
, Handling floating-point exceptions in numeric programs, ACM Transactions on Programming Languages and Systems, vol.18, issue.2, pp.139-174, 1996.
DOI : 10.1145/227699.227701
, Deciding floating-point logic with systematic abstraction, FMCAD, pp.131-140, 2012.
, Number types, CGAL User and Reference Manual. CGAL Editorial Board, 2000.
, Accuracy and stability of numerical algorithms, SIAM, 2002.
DOI : 10.1137/1.9780898718027
, Type classes and filters for mathematical analysis in Isabelle/HOL, Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP), pp.279-294, 2013.
, The computation of transcendental functions on the IA-64 architecture, Intel Technology Journal, 1999.
, Algorithms for quad-double precision floating point arithmetic, Proceedings 15th IEEE Symposium on Computer Arithmetic. ARITH-15 2001, pp.155-162, 2001.
DOI : 10.1109/ARITH.2001.930115
, Behavioral interface specification languages, ACM Computing Surveys, vol.44, issue.3, p.16, 2012.
DOI : 10.1145/2187671.2187678
, Using Dafny, an Automatic Program Verifier, Tools for Practical Software Verification, pp.156-181, 2012.
DOI : 10.1007/978-3-540-78800-3_24
, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259
, Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL, Interactive Theorem Proving, pp.377-392, 2012.
DOI : 10.1007/978-3-642-32347-8_26
, Synthesizing accurate floating-point formulas, 2013 IEEE 24th International Conference on Application-Specific Systems, Architectures and Processors, pp.113-116, 2013.
DOI : 10.1109/ASAP.2013.6567563
URL : https://hal.archives-ouvertes.fr/hal-00835736
, Formally Verified Computation of Enclosures of Solutions of Ordinary Differential Equations, NASA Formal Methods, pp.113-127, 2014.
DOI : 10.1007/978-3-319-06200-6_9
, Formal verification of a theory of IEEE rounding, 14th International Conference on Theorem Proving in Higher Order Logics, pp.239-254, 2001.
, Formal Verification of a Fully IEEE Compliant Floating Point Unit, 2002.
, Formal verification of the VAMP floating point unit. Formal Methods in System Design, pp.227-266, 2005.
, Further analysis of Kahan???s algorithm for the accurate computation of $2\times 2$ determinants, Mathematics of Computation, vol.82, issue.284, pp.2245-2264, 2013.
DOI : 10.1090/S0025-5718-2013-02679-8
, Miscalculating Area and Angles of a Needle-like Triangle . Unpublished manuscript, 1986.
, On the Cost of Floating-Point Computation Without Extra- Precise Arithmetic. Unpublished manuscript, 2004.
, Michael Norrish, et al. seL4: Formal verification of an OS kernel, Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pp.207-220, 2009.
, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems, vol.4, issue.2, pp.123-193, 1999.
DOI : 10.1145/307988.307989
, Proof engineering in the large: formal verification of Pentium???4 floating-point divider, International Journal on Software Tools for Technology Transfer (STTT), vol.4, issue.3, pp.323-334, 2003.
DOI : 10.1007/s10009-002-0081-6
, Computer-Aided Reasoning: An Approach, 2000.
, The Art of Computer Programming: Seminumerical Algorithms, 1997.
, Digit selection for SRT division and square root, IEEE Transactions on Computers, vol.54, issue.3, pp.294-303, 2005.
DOI : 10.1109/TC.2005.47
, Theorems on efficient argument reductions, 16th IEEE Symposium on Computer Arithmetic, 2003. Proceedings., pp.129-136, 2003.
DOI : 10.1109/ARITH.2003.1207670
URL : https://hal.archives-ouvertes.fr/hal-00156244
, Not a number of floating point problems, Journal of Object Technology, vol.5, issue.2, pp.75-83, 2006.
, Erreurs de mathématiciens des origines à nos jours. Castaigne, 1935.
, Dafny: An automatic program verifier for functional correctness, Logic for Programming, Artificial Intelligence, and Reasoning, pp.348-370, 2010.
, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861
, Worst cases for correct rounding of the elementary functions in double precision, Proceedings 15th IEEE Symposium on Computer Arithmetic. ARITH-15 2001, pp.111-118, 2001.
DOI : 10.1109/ARITH.2001.930110
, Différentiabilité et intégrabilité en Coq Application à la formule de d'Alembert, Vingt-troisièmes Journées Francophones des Langages Applicatifs, 2012.
, Mechanizing proof: computing, risk, and trust, 2004.
, Algorithms to reveal properties of floating-point arithmetic, Commun. ACM, vol.15, issue.11, pp.949-951, 1972.
, Jessie, Proceedings of the 2007 workshop on Programming languages meets program verification , PLPV '07, pp.1-2, 2007.
DOI : 10.1145/1292597.1292598
, Formalisation et automatisation de preuves en analyses rélle et numérique, 2001.
, Some issues related to double rounding, BIT Numerical Mathematics, vol.18, issue.2, pp.897-924, 2013.
DOI : 10.1007/s10543-013-0436-2
, Floating-point arithmetic in the Coq system, Information and Computation, vol.216, pp.14-23, 2012.
DOI : 10.1016/j.ic.2011.09.005
URL : https://hal.archives-ouvertes.fr/hal-00797913
, Defining the IEEE-854 floating-point standard in PVS, 1995.
, Verification of IEEE compliant subtractive division algorithms, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, pp.64-78, 1996.
, A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program, IEEE Transactions on Computers, vol.47, issue.9, pp.913-926, 1998.
DOI : 10.1109/12.713311
, Certifying algorithms, Computer Science Review, vol.5, issue.2, pp.119-161, 2011.
DOI : 10.1016/j.cosrev.2010.09.009
, 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
, Formally certified floating-point filters for homogeneous geometric predicates, Theoretical Informatics and Applications, pp.57-70, 2007.
DOI : 10.1051/ita:2007005
URL : https://hal.archives-ouvertes.fr/inria-00071232
, The Picard Algorithm for Ordinary Differential Equations in Coq, Interactive Theorem Proving, pp.463-468, 2013.
DOI : 10.1007/978-3-642-39634-2_34
, KB3D reference manual -version 1.a, pp.23681-2199, 2005.
, On Taylor Model Based Integration of ODEs, SIAM Journal on Numerical Analysis, vol.45, issue.1, pp.236-262, 2007.
DOI : 10.1137/050638448
, A Brief Overview of Mizar, Proceedings of the 22th International Conference on Theorem Proving in Higher Order Logics, pp.67-72, 2009.
DOI : 10.1007/3-540-44755-5_26
, Hardware-dependent proofs of numerical programs, Certified Programs and Proofs, pp.314-329, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00772508
, Accurate Sum and Dot Product, SIAM Journal on Scientific Computing, vol.26, issue.6, pp.1955-1988, 2005.
DOI : 10.1137/030601818
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.1547
, PVS: A prototype verification system, 11th International Conference on Automated Deduction, pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217
, Formally verifying IEEE compliance of floating point hardware, Intel Technology Journal, vol.3, issue.1, 1999.
, Verifying (in-) stability in floatingpoint programs by increasing precision, using SMT solving, 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. SYNASC, 2013.
, Software verification with verifast: Industrial case studies, Science of Computer Programming, vol.14, issue.821, pp.77-97, 2014.
, Verifying floating-point programs with constraint programming and abstract interpretation techniques, Automated Software Engineering, vol.34, issue.1, pp.1-27, 2014.
DOI : 10.1007/s10515-014-0154-2
URL : https://hal.archives-ouvertes.fr/hal-00860681
, How to believe a machine-checked proof. Twenty Five Years of Constructive Type Theory, p.205, 1998.
, Keymaera: A hybrid theorem prover for hybrid systems, Automated Reasoning, pp.171-178, 2008.
, Algorithms for arbitrary precision floating point arithmetic, [1991] Proceedings 10th IEEE Symposium on Computer Arithmetic, pp.132-143, 1991.
DOI : 10.1109/ARITH.1991.145549
, Subtypes for specifications: predicate subtyping in PVS, IEEE Transactions on Software Engineering, vol.24, issue.9, pp.709-720, 1998.
DOI : 10.1109/32.713327
, Innocuous double rounding of basic arithmetic operations, Journal of Formalized Reasoning, vol.7, issue.1, p.2014
URL : https://hal.archives-ouvertes.fr/hal-01091186
, Combining ACL2 and an automated verification tool to verify a multiplier, Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications , ACL2 '06, pp.63-70, 2006.
DOI : 10.1145/1217975.1217990
, A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor, LMS Journal of Computation and Mathematics, vol.1, pp.148-200, 1998.
, A mechanically checked proof of correctness of the AMD- K5 floating point square root microcode. Formal Methods in System Design, p.75, 1999.
, A case study in formal verification of register-transfer logic with ACL2: The floating point adder of the AMD Athlon processor, LNCS, pp.3-36, 1954.
, Computation and formal verification of SRT quotient and square root digit selection tables, IEEE Transactions on Computers, vol.62, issue.5, pp.900-913, 2013.
, An SMT-LIB theory of binary floating-point arithmetic, International Workshop on Satisfiability Modulo Theories (SMT), 2010.
, Computing predecessor and successor in rounding to??nearest, BIT Numerical Mathematics, vol.31, issue.1, pp.419-431, 2009.
DOI : 10.1007/s10543-009-0218-z
URL : https://hal.archives-ouvertes.fr/inria-00337537
, Mechanical Verification of a Square Root Algorithm Using Taylor???s Theorem, Formal Methods in Computer-Aided Design, pp.274-291, 2002.
DOI : 10.1007/3-540-36126-X_17
, Adaptive precision floating-point arithmetic and fast robust geometric predicates, Discrete and Computational Geometry, pp.305-363, 1997.
, FPU Implementations with Denormalized Numbers, IEEE Transactions on Computers, vol.54, issue.7, pp.825-836, 2005.
DOI : 10.1109/TC.2005.118
, Floating point computation, 1974.
, Some features of the Mizar language, Proceedings of the ESPRIT Workshop, 1993.
, The Lorenz attractor exists Comptes Rendus de l'Académie des Sciences-Series I-Mathematics, pp.1197-1202, 1999.
, Validated numerics: a short introduction to rigorous computations, 2011.
, ALGOL procedures voor het rekenen in dubbele lengte, RC-Informatie, vol.21, 1969.
, Automated proofs of object code for a widely used microprocessor, 1992.
, An integrated proof language for imperative programs, ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2009.
, Using symbolic execution to verify the order of accuracy of numerical approximations, 2014.
, Formal Global Optimisation with Taylor Models, Automated Reasoning, pp.408-422, 2006.
DOI : 10.1007/11814771_35