UTC Time, Formally Verified - Presentation at CPP 2024

Explore a 31-minute conference talk from CPP 2024 detailing the FV Time project, a small-scale verification effort developed in the Coq proof assistant using Mathematical Components libraries. Delve into the implementation of a library for managing conversions between UTC and timestamp formats, including the novel incorporation of leap seconds. Gain insights into the methodology for verifying software with Coq, as presenters discuss key challenges faced during development and showcase general-purpose solutions applicable to other verification projects. Learn about a refinement package bridging proof-oriented MathComp numbers with computation-oriented primitive numbers from Coq's standard library, and discover tactics for automating proofs of decidable statements over finite ranges through brute-force computation.