Flocq

Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 20 articles )

Showing results 1 to 20 of 20.
Sorted by year (citations)

  1. Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang: Deductive verification of floating-point Java programs in KeY (2021)
  2. Ishii, Daisuke; Yabu, Tomohito: Computer-assisted verification of four interval arithmetic operators (2020)
  3. Bertot, Yves; Rideau, Laurence; Théry, Laurent: Distant decimals of (\pi): formal proofs of some algorithms computing them and guarantees of exact computation (2018)
  4. Muller, Jean-Michel; Brunie, Nicolas; de Dinechin, Florent; Jeannerod, Claude-Pierre; Joldes, Mioara; Lefèvre, Vincent; Melquiond, Guillaume; Revol, Nathalie; Torres, Serge: Handbook of floating-point arithmetic (2018)
  5. Boldo, Sylvie: Computing a correct and tight rounding error bound using rounding-to-nearest (2017)
  6. Boldo, Sylvie; Joldes, Mioara; Muller, Jean-Michel; Popescu, Valentina: Formal verification of a floating-point expansion renormalization algorithm (2017)
  7. Magron, Victor; Constantinides, George; Donaldson, Alastair: Certified roundoff error bounds using semidefinite programming (2017)
  8. Krebbers, Robbert: A formal C memory model for separation logic (2016)
  9. Martin-Dorel, Érik; Melquiond, Guillaume: Proving tight bounds on univariate expressions with elementary functions in Coq (2016)
  10. Roux, Pierre: Formal proofs of rounding error bounds. With application to an automatic positive definiteness check (2016)
  11. Boldo, Sylvie: Stupid is as stupid does: taking the square root of the square of a floating-point number (2015)
  12. Boldo, Sylvie; Jourdan, Jacques-Henri; Leroy, Xavier; Melquiond, Guillaume: Verified compilation of floating-point computations (2015)
  13. Jacobsen, Charles; Solovyev, Alexey; Gopalakrishnan, Ganesh: A parameterized floating-point formalizaton in HOL Light (2015)
  14. Roux, Pierre; Garoche, Pierre-Loïc: Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case (2015)
  15. Boldo, Sylvie; Clément, François; Filliâtre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Trusting computations: a mechanized proof from partial differential equations to actual program (2014)
  16. Roux, Pierre: Innocuous double rounding of basic arithmetic operations (2014)
  17. Boldo, Sylvie; Clément, François; Filliâtre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Wave equation numerical resolution: a comprehensive mechanized proof of a C program (2013)
  18. Krebbers, Robbert; Spitters, Bas: Type classes for efficient exact real arithmetic in \textscCoq (2013)
  19. Collins, Pieter; Niqui, Milad; Revol, Nathalie: A validated real function calculus (2011)
  20. Krebbers, Robbert; Spitters, Bas: Computer certified efficient exact reals in Coq (2011)