 | 2009 |
|---|
| 14 |       | Sylvie Boldo,
Jean-Christophe Filliâtre,
Guillaume Melquiond:
Combining Coq and Gappa for Certifying Floating-Point Programs.
Calculemus/MKM 2009: 59-74 |
| 13 | | Sylvie Boldo:
Floats and Ropes: A Case Study for Formal Numerical Program Verification.
ICALP (2) 2009: 91-102 |
| 12 | | Sylvie Boldo:
Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven.
IEEE Trans. Computers 58(2): 220-225 (2009) |
| 2008 |
|---|
| 11 | | Sylvie Boldo,
Guillaume Melquiond:
Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd.
IEEE Trans. Computers 57(4): 462-471 (2008) |
| 2007 |
|---|
| 10 | | Sylvie Boldo,
Jean-Christophe Filliâtre:
Formal Verification of Floating-Point Programs.
IEEE Symposium on Computer Arithmetic 2007: 187-194 |
| 9 | | Sylvie Boldo,
Marc Daumas,
Ren-Cang Li:
Formally Verified Argument Reduction with a Fused-Multiply-Add
CoRR abs/0708.3722: (2007) |
| 2006 |
|---|
| 8 | | Sylvie Boldo:
Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms.
IJCAR 2006: 52-66 |
| 7 | | Sylvie Boldo,
César Muñoz:
Provably faithful evaluation of polynomials.
SAC 2006: 1328-1332 |
| 2005 |
|---|
| 6 | | Sylvie Boldo,
Jean-Michel Muller:
Some Functions Computable with a Fused-Mac.
IEEE Symposium on Computer Arithmetic 2005: 52-58 |
| 2004 |
|---|
| 5 | | Sylvie Boldo,
Marc Daumas:
Properties of two's complement floating point notations.
STTT 5(2-3): 237-246 (2004) |
| 2003 |
|---|
| 4 | | Ren-Cang Li,
Sylvie Boldo,
Marc Daumas:
Theorems on Efficient Argument Reductions.
IEEE Symposium on Computer Arithmetic 2003: 129-136 |
| 3 | | Sylvie Boldo,
Marc Daumas:
Representable Correcting Terms for Possibly Underflowing Floating Point Operations.
IEEE Symposium on Computer Arithmetic 2003: 79-86 |
| 2002 |
|---|
| 2 | | Sylvie Boldo,
Marc Daumas:
Properties of the subtraction valid for any floating point system.
Electr. Notes Theor. Comput. Sci. 66(2): (2002) |
| 2001 |
|---|
| 1 | | Sylvie Boldo,
Marc Daumas,
Claire Moreau-Finot,
Laurent Théry:
Computer validated proofs of a toolset for adaptable arithmetic
CoRR cs.MS/0107025: (2001) |
