@inproceedings{cda9080204f743298b2d83e3db791650,
title = "VCFloat2: Floating-Point Error Analysis in Coq",
abstract = "The development of sound and efficient tools that automatically perform floating-point round-off error analysis is an active area of research with applications to embedded systems and scientific computing. In this paper we describe VCFloat2, a novel extension to the VCFloat tool for verifying floating-point C programs in Coq. Like VCFloat1, VCFloat2 soundly and automatically computes round-off error bounds on floating-point expressions, but does so to higher accuracy; with better performance; with more generality for nonstandard number formats; with the ability to reason about external (user-defined or library) functions; and with improved modularity for interfacing with other program verification tools in Coq. We evaluate the performance of VCFloat2 using common benchmarks; compared to other state-of-the art tools, VCFloat2 computes competitive error bounds and transparent certificates that require less time for verification.",
keywords = "floating point, round-off error analysis",
author = "Andrew Appel and Ariel Kellison",
note = "Publisher Copyright: {\textcopyright} 2024 Owner/Author.; 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, in affiliation with the annual Symposium on Principles of Programming, Languages, ,POPL 2024 ; Conference date: 15-01-2024 Through 16-01-2024",
year = "2024",
month = jan,
day = "9",
doi = "10.1145/3636501.3636953",
language = "English (US)",
series = "CPP 2024 - Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with: POPL 2024",
publisher = "Association for Computing Machinery, Inc",
pages = "14--29",
editor = "Amin Timany and Dmitriy Traytel and Brigitte Pientka and Sandrine Blazy",
booktitle = "CPP 2024 - Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with",
}