POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Mon 15 Jan 2024 12:00 - 12:30 at Kelvin Lecture - Compiler / Program Verification Chair(s): Vadim Zaliva

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 VCFloat, 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.

Mon 15 Jan

Displayed time zone: London change

11:00 - 12:30
Compiler / Program VerificationCPP at Kelvin Lecture
Chair(s): Vadim Zaliva University of Cambridge, UK
11:00
30m
Talk
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
CPP
Philipp G. Haselwarter Aarhus University, Benjamin Salling Hvass Aarhus University, Lasse Letager Hansen Aarhus University, Théo Winterhalter INRIA Saclay, Cătălin Hriţcu MPI-SP, Bas Spitters Aarhus University
Pre-print File Attached
11:30
30m
Talk
UTC time, formally verified
CPP
Ana de Almeida Borges University of Barcelona and Formal Vindications S.L., Mireia González Bedmar University of Barcelona and Formal Vindications S.L., Juan Conejero Rodríguez University of Barcelona and Formal Vindications S.L., Eduardo Hermo Reyes University of Barcelona and Formal Vindications S.L., Joaquim Casals Buñuel University of Barcelona and Formal Vindications S.L., Joost J. Joosten University of Barcelona
12:00
30m
Talk
VCFloat2: Floating-point error analysis in Coq
CPP
Andrew W. Appel Princeton University, Ariel E. Kellison Cornell University
Pre-print