8 citations · 20 across the 10 of their papers we have counts for
10 papers
Using Graphics Processors for Parallelizing Hash-based Data Carving
Sylvain Collange, Yoginder Dandass, Marc Daumas +1
The ability to detect fragments of deleted image files and to reconstruct these image files from all available fragments on disk is a key activity in the field of digital forensics…
Formally Verified Argument Reduction with a Fused-Multiply-Add
Sylvie Boldo, Marc Daumas, Ren Cang Li
Cody & Waite argument reduction technique works perfectly for reasonably large arguments but as the input grows there are no bit left to approximate the constant with enough accura…
Verified Real Number Calculations: A Library for Interval Arithmetic
Marc Daumas, David Lester, César Muñoz
Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a th…
Graphic processors to speed-up simulations for the design of high performance solar receptors
Sylvain Collange, Marc Daumas, David Defour
Graphics Processing Units (GPUs) are now powerful and flexible systems adapted and used for other purposes than graphics calculations (General Purpose computation on GPU -- GPGPU).…
Formal proof for delayed finite field arithmetic using floating point operators
Sylvie Boldo, Marc Daumas, Pascal Giorgi
Formal proof checkers such as Coq are capable of validating proofs of correction of algorithms for finite field arithmetics but they require extensive training from potential users…
Certification of bounds on expressions involving rounded operators
Marc Daumas, Guillaume Melquiond
Gappa uses interval arithmetic to certify bounds on mathematical expressions that involve rounded as well as exact operators. Gappa generates a theorem with its proof for each boun…