The following pages link to (Q4790659):
Displaying 25 items.
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952) (← links)
- Deciding floating-point logic with abstract conflict driven clause learning (Q479837) (← links)
- Floating-point arithmetic in the Coq system (Q714617) (← links)
- Formal verification of the VAMP floating point unit (Q816201) (← links)
- Formalization of fixed-point arithmetic in HOL (Q816219) (← links)
- Semantics of roundoff error propagation in finite precision calculations (Q853732) (← links)
- Additive symmetries: The non-negative case. (Q1853635) (← links)
- Formal verification of numerical programs: from C annotated programs to mechanical proofs (Q1949765) (← links)
- A validated real function calculus (Q1949769) (← links)
- Computing predecessor and successor in rounding to nearest (Q2391021) (← links)
- Trusting computations: a mechanized proof from partial differential equations to actual program (Q2398899) (← links)
- A parameterized floating-point formalizaton in HOL Light (Q2520685) (← links)
- Motivations for an arbitrary precision interval arithmetic and the MPFI library (Q2572919) (← links)
- Proving Bounds on Real-Valued Functions with Computations (Q3541683) (← links)
- Combining Coq and Gappa for Certifying Floating-Point Programs (Q3637269) (← links)
- An accurate elementary mathematical library for the IEEE floating point standard (Q4371730) (← links)
- FloatX (Q4960963) (← links)
- Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic” (Q5066604) (← links)
- Floating-Point LLL: Theoretical and Practical Aspects (Q5188541) (← links)
- Multi-Prover Verification of Floating-Point Programs (Q5747756) (← links)
- The Design of Core 2: A Library for Exact Numeric Computation in Geometry and Algebra (Q5747872) (← links)
- Floating-point arithmetic (Q6047500) (← links)
- Finding normal binary floating-point factors efficiently (Q6156639) (← links)
- Automatic Generation of Guard-Stable Floating-Point Code (Q6487928) (← links)
- Provably correct floating-point implementation of a point-in-polygon algorithm (Q6535939) (← links)
