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.

• Type: Conference
• Year: 2010
• Where: CADE
• Authors: Ali Ayad, Claude Marché
• Keywords: CADE 2010, Deductive Program Verification, First-order Axiomatization, Interactive Proof Assistants, Logical Reasoning