Sylvie Boldo
Sylvie Boldo
Inria, LRI, University Paris Sud, CNRS
Підтверджена електронна адреса в inria.fr - Домашня сторінка
Назва
Посилання
Посилання
Рік
IEEE standard for floating-point arithmetic
D Zuras, M Cowlishaw, A Aiken, M Applegate, D Bailey, S Bass, ...
IEEE Std 754 (2008), 1-70, 2008
2002008
Flocq: A unified library for proving floating-point algorithms in Coq
S Boldo, G Melquiond
2011 IEEE 20th Symposium on Computer Arithmetic, 243-252, 2011
1442011
Formal verification of floating-point programs
S Boldo, JC Filliâtre
18th IEEE Symposium on Computer Arithmetic (ARITH'07), 187-194, 2007
1212007
Coquelicot: A user-friendly library of real analysis for Coq
S Boldo, C Lelay, G Melquiond
Mathematics in Computer Science 9 (1), 41-62, 2015
942015
Combining Coq and Gappa for certifying floating-point programs
S Boldo, JC Filliâtre, G Melquiond
International Conference on Intelligent Computer Mathematics, 59-74, 2009
872009
Wave equation numerical resolution: a comprehensive mechanized proof of a C program
S Boldo, F Clément, JC Filliâtre, M Mayero, G Melquiond, P Weis
Journal of Automated Reasoning 50 (4), 423-456, 2013
822013
Emulation of a FMA and correctly rounded sums: Proved algorithms using rounding to odd
S Boldo, G Melquiond
IEEE Transactions on Computers 57 (4), 462-471, 2008
582008
Preuves formelles en arithmétiques à virgule flottante
S Boldo
Lyon, École normale supérieure (sciences), 2004
572004
A formally-verified C compiler supporting floating-point arithmetic
S Boldo, JH Jourdan, X Leroy, G Melquiond
2013 IEEE 21st Symposium on Computer Arithmetic, 107-115, 2013
542013
Formalization of real analysis: A survey of proof assistants and libraries
S Boldo, C Lelay, G Melquiond
Mathematical Structures in Computer Science 26 (7), 1196-1233, 2016
522016
Verified compilation of floating-point computations
S Boldo, JH Jourdan, X Leroy, G Melquiond
Journal of Automated Reasoning 54 (2), 135-163, 2015
442015
Representable correcting terms for possibly underflowing floating point operations
S Boldo, M Daumas
Proceedings 2003 16th IEEE Symposium on Computer Arithmetic, 79-86, 2003
432003
Formal proof of a wave equation resolution scheme: the method error
S Boldo, F Clément, JC Filliâtre, M Mayero, G Melquiond, P Weis
International Conference on Interactive Theorem Proving, 147-162, 2010
402010
Theorems on efficient argument reductions
RC Li, S Boldo, M Daumas
Proceedings 2003 16th IEEE Symposium on Computer Arithmetic, 129-136, 2003
382003
Hardware-independent proofs of numerical programs
S Boldo, TMT Nguyen
Second NASA Formal Methods Symposium (NFM 2010), 14-23, 2010
372010
A simple test qualifying the accuracy of Horner's rule for polynomials
S Boldo, M Daumas
Numerical Algorithms 37 (1), 45-60, 2004
352004
Formal verification of numerical programs: from C annotated programs to mechanical proofs
S Boldo, C Marché
Mathematics in Computer Science 5 (4), 377-393, 2011
342011
Some functions computable with a fused-mac
S Boldo, JM Muller
17th IEEE Symposium on Computer Arithmetic (ARITH'05), 52-58, 2005
322005
Formal proof for delayed finite field arithmetic using floating point operators
S Boldo, M Daumas, P Giorgi
arXiv preprint cs/0703026, 2007
31*2007
Trusting computations: a mechanized proof from partial differential equations to actual program
S Boldo, F Clément, JC Filliâtre, M Mayero, G Melquiond, P Weis
Computers & Mathematics with Applications 68 (3), 325-352, 2014
272014
У даний момент система не може виконати операцію. Спробуйте пізніше.
Статті 1–20