VCFloat2: Floating-Point Error Analysis in Coq

Andrew Appel, Ariel Kellison

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationCPP 2024 - Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with
Subtitle of host publicationPOPL 2024
EditorsAmin Timany, Dmitriy Traytel, Brigitte Pientka, Sandrine Blazy
PublisherAssociation for Computing Machinery, Inc
Pages14-29
Number of pages16
ISBN (Electronic)9798400704888
DOIs
StatePublished - Jan 9 2024
Event13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, in affiliation with the annual Symposium on Principles of Programming, Languages, ,POPL 2024 - London, United Kingdom
Duration: Jan 15 2024Jan 16 2024

Publication series

NameCPP 2024 - Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with: POPL 2024

Conference

Conference13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, in affiliation with the annual Symposium on Principles of Programming, Languages, ,POPL 2024
Country/TerritoryUnited Kingdom
CityLondon
Period1/15/241/16/24

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Software

Keywords

  • floating point
  • round-off error analysis

Fingerprint

Dive into the research topics of 'VCFloat2: Floating-Point Error Analysis in Coq'. Together they form a unique fingerprint.

Cite this