Verified compilation of floating-point computations

DOI10.1007/s10817-014-9317-xzbMath1331.68047OpenAlexW1988579293MaRDI QIDQ2352505

Guillaume Melquiond, Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy

Publication date: 2 July 2015

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-00862689v3/file/floating-point-compcert.pdf

zbMATH Keywords

floating-point arithmeticCoqcompiler verificationsemantic preservationCompCert

Mathematics Subject Classification ID

Related Items (4)

A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Trace-Relating Compiler Correctness and Secure Compilation ⋮ Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic” ⋮ Enabling floating-point arithmetic in the Coq proof assistant

Uses Software

• Coq
• Flocq
• CompCert
• ASTREE

Cites Work

• A floating-point technique for extending the available precision
• Hardware-Dependent Proofs of Numerical Programs
• Handbook of Floating-Point Arithmetic
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor
• Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd
• Accurate Floating-Point Summation Part I: Faithful Rounding
• Programming Languages and Systems
• Multi-Prover Verification of Floating-Point Programs
• Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
• Unnamed Item

This page was built for publication: Verified compilation of floating-point computations