The team has developed a Coq verified library for time conversions between UTC and Unix, including leap seconds [to be published]. More precisely, the Coq Time Library is a verification project consisting of a library for managing conversions between formats of time (UTC and timestamp), as well as some commonly used functions like sums, computation of a duration between two times, etc.
What is a Time manager
Time manager definition:
Set of algorithms which define the time and arithmetic among dates (add time; difference, etc.). In fact, any programming framework or operating system have their on time manager).
Example of study: different driving times of the same vehicle depending of the time manager used.
We present our FV Time Manager, a formally verified software for managing UTC time, which provides public formal specifications, public software, and public mathematical proofs.
The only fully UTC consistent, time format and timestamp.
UTC Timespan 1577836827
Formal calendar definition (different from Gregorian UTC calendar) for time interval measurement as general solution for the problem of grouping seconds in UTC calendars.
Try the time manager onlineTry it now