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)