Icing: supporting fast-math style optimizations in a verified compiler

DOI10.1007/978-3-030-25543-5_10MaRDI QIDQ6154878zbMATH OpenOpenAlexFDO

Authors Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock

Publication date 16 February 2024

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-25543-5_10

zbMATH Keywords

compiler verificationfloating-point arithmeticoptimization

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verified compilation of floating-point computations
• The verified CakeML compiler backend
• A Framework for Formal Verification of Compiler Optimizations
• A formally verified compiler back-end
• CompCertTSO

Cited in

(1)

• BMOA: Baseline-Mechanism-Outcome Attribution for Compiler-Induced Numerical Deviations

This page was built for publication: Icing: supporting fast-math style optimizations in a verified compiler

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6154878)