Formally-verified round-off error analysis of Runge-Kutta methods. (English) Zbl 07800194
MSC:
68V15
Found 18 Documents (Results 1–18)
Formal verification of transcendental fixed- and floating-point algorithms using an automatic theorem prover. (English) Zbl 1522.68306
Formalization of double-word arithmetic, and comments on “Tight and rigorous error bounds for basic building blocks of double-word arithmetic”. (English) Zbl 07500134
MSC:
65-XX
Deductive verification of floating-point Java programs in KeY. (English) Zbl 1474.68186
Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 242-261 (2021).
Primitive floats in Coq. (English) Zbl 07649956
Harrison, John (ed.) et al., 10th international conference on interactive theorem proving, ITP 2019, September 9–12, 2019, Portland, OR, USA. Proceedings. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 141, Article 7, 20 p. (2019).
MSC:
68V15
Handbook of floating-point arithmetic. 2nd edition. (English) Zbl 1394.65001
Cham: Birkhäuser (ISBN 978-3-319-76525-9/hbk; 978-3-319-76526-6/ebook). xxv, 627 p. (2018).
Reviewer: T. C. Mohan (Chennai)
Formal verification of a floating-point expansion renormalization algorithm. (English) Zbl 1483.68479
Ayala-Rincón, Mauricio (ed.) et al., Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10499, 98-113 (2017).
Formal proofs of rounding error bounds. With application to an automatic positive definiteness check. (English) Zbl 1409.68263
MSC:
68T15
65G50
Proving tight bounds on univariate expressions with elementary functions in Coq. (English) Zbl 1386.68151
A parameterized floating-point formalizaton in HOL Light. (English) Zbl 1352.65667
Bogomolov, Sergiy (ed.) et al., Selected papers based on the presentations at the 7th and 8th international workshops on numerical software verification (NSV), Vienna, Austria, July 17–18, 2014 and April 13, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 317, 101-107 (2015).
Stupid is as stupid does: taking the square root of the square of a floating-point number. (English) Zbl 1352.65664
Bogomolov, Sergiy (ed.) et al., Selected papers based on the presentations at the 7th and 8th international workshops on numerical software verification (NSV), Vienna, Austria, July 17–18, 2014 and April 13, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 317, 27-32 (2015).
Filter Results by …
Document Type
- Journal Articles (12)
- Collection Articles (5)
- Books (1)
all
top 5
Author
- Melquiond, Guillaume (4)
- Roux, Pierre (4)
- Boldo, Sylvie (3)
- Martin-Dorel, Érik (3)
- Muller, Jean-Michel (3)
- Joldeş, Mioara (2)
- Revol, Nathalie (2)
- Abbasi, Rosa (1)
- Ahrendt, Wolfgang (1)
- Andrlon, Mak (1)
- Bertholon, Guillaume (1)
- Brunie, Nicolas (1)
- Collins, Peter J. (1)
- Coward, Samuel (1)
- Darulova, Eva (1)
- de Dinechin, Florent (1)
- Donaldson, Alastair F. (1)
- Drane, Theo A. (1)
- Faissole, Florian (1)
- Gopalakrishnan, Ganesh Lalitha (1)
- Ishii, Daisuke (1)
- Jacobsen, Charles (1)
- Jeannerod, Claude-Pierre (1)
- Jourdan, Jacques-Henri (1)
- Lefèvre, Vincent (1)
- Leroy, Xavier (1)
- Magron, Victor (1)
- Morini, Emiliano (1)
- Niqui, Milad (1)
- Paulson, Lawrence Charles (1)
- Popescu, Valentina (1)
- Rideau, Laurence (1)
- Schiffl, Jonas (1)
- Solovyev, Alexey (1)
- Torres, Serge (1)
- Ulbrich, Mattias (1)
- Yabu, Tomohito (1)
all
top 3
Software
- Flocq (18)
- Coq (14)
- HOL Light (5)
- MPFR (4)
- mctoolbox (4)
- ACL2 (3)
- CAMPARY (3)
- MetiTarski (3)
- Sollya (3)
- dReal (3)
- z3 (3)
- Apron (2)
- Archive Formal Proofs (2)
- CR-LIBM (2)
- CRlibm (2)
- Coq Interval (2)
- Frama-C (2)
- Gappa (2)
- HOL (2)
- INTLAB (2)
- Isabelle/HOL (2)
- PVS (2)
- RODES (2)
- SMT-LIB (2)
- Why3 (2)
- ARPREC (1)
- ASTREE (1)
- Alt-Ergo (1)
- Boogie (1)
- CBench (1)
- CUDA (1)
- CVC4 (1)
- CompCert (1)
- Coquelicot (1)
- Cosy (1)
- DPE (1)
- Daisy (1)
- FLIP (1)
- FPTaylor (1)
- FloPoCo (1)
- GRKLib (1)
- HolPy (1)
- IEEE_Floating_Point (1)
- JBMC (1)
- KRAKATOA (1)
- KeY (1)
- MACHAR (1)
- MPFI (1)
- Magma (1)
- MathSAT5 (1)
- Mathematica (1)
- Maxima (1)
- Metis_ (1)
- Mosek (1)
- NLCertify (1)
- NTL (1)
- Nagini (1)
- OCaml (1)
- OpenJML (1)
- QEPCAD (1)
- QF_FP (1)
- SDPA (1)
- SMTCoq (1)
- SoftFloat (1)
- Toolchain (1)
- ValidSDP (1)
- VeriFast (1)
- Viper (1)
- chebop (1)
- doubledouble (1)
- fpLLL (1)
- gmp (1)
- kepler98 (1)
- kv (1)
- mftoolbox (1)
