The FV Time Manager


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.

There are of course many libraries to perform conversions between time formats. However, our library incorporates two crucial aspects:

(a) It includes leap seconds. Leap seconds are part of the UTC standard, but they are not usually counted in this kind of general-purpose libraries, because the error is small and irrelevant for many purposes. However, it can be relevant for some, like computations that are meant to enforce a law or regulation, or for critical systems.

(b) It is formally verified, which means that we provide computer-checked mathematical proof that the algorithms to perform time conversions behave exactly according to a simple, human-readable specification.

The FV Time Manager is the extraction of these verified algorithms to a computer-efficient language like OCaml, so that it can be used as time manager in industrial projects. Our team can also provide wrappers to other programming languages to facilitate the integration of the manager in developments.

Contributions to the Coq Proof Assistant


Primitive machine signed integers for Coq hah

https://coq.github.io/doc/master/stdlib/Coq.Numbers.Cyclic.Int63.Sint63.html

An important issue for the use of Coq in industrial developments is its treatment of natural numbers and integers. As a mathematical programming language, Coq defines these numbers in a way that is useful to prove theorems about them, but is too inefficient to use in practical executions. To solve this problem, recently Coq introduced the Int63 type, which gives efficient machine unsigned integers available inside Coq. However, signed integers continued being unavailable, so the \textit{Prometheuss - Proof Methods for European Software Systems} team contributed them to Coq. They are called Sint63 and are now part of the latest Coq development branch, and will be part of the next official release of a Coq version.


A Coq tool for proof automation of bounded arithmetical inequalities (to be published)

After facing the frequent practical problem of bounding an arithmetical expression (for instance, to prove that overflow will not occur) and experiencing the intrinsic difficulties of proving such inequalities using mathematical arguments inside Coq, the team was able to develop a tool for automating this kind of task. In particular, the tool instructs Coq to the extent that it can compute all the cases and check that the inequality holds for each of them, and thus deduce that the inequality holds in general. This tool is developed for inequalities on types Int63 and Sint63, and is planned to be released for other Coq types.


An extension of the SSReflect library with functions about sequences (to be published)

The SSReflect library for sequences (https://math-comp.github.io/htmldoc/mathcomp.ssreflect.seq.html) does not include any functions to check whether a sequence is a subchain of another one, i.e., a consecutive subsequence. Our team developed this function, together with suffix and prefix, and all the required theorems about them to contribute to the MathComp SSReflect library.


Analysis of the road transportation sector