Multi-Prover Verification of Floating-Point Programs

12 years 22 days ago
Multi-Prover Verification of Floating-Point Programs
Abstract. In the context of deductive program verification, supporting floatingpoint computations is tricky. We propose an expressive language to formally specify behavioral properties of such programs. We give a first-order axiomatization of floating-point operations which allows to reduce verification to checking the validity of logic formulas, in a suitable form for a large class of provers including SMT solvers and interactive proof assistants. Experiments using the Frama-C platform for static analysis of C code are presented.
Ali Ayad, Claude Marché
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where CADE
Authors Ali Ayad, Claude Marché
Comments (0)