Find out what we have been working on!
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.
An analysis of the European tachograph technology and EU Regulations 3821/85, 799/2016, and 561/06. See the analysis document. A preliminar analysis of the American ELD technology and regulations USA CFR 49 Part 395 and Canada SOR/2005-313 (to be published).
Our contributions to the Coq verification ecosystem
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.
See 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.
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.
This paper analyses a selection of articles from European transport regulations that contain algorithmic information, but may be problematic to implement. We focus on issues regarding the interpretation of tachograph data and requirements on weekly rest periods. We first show that the interpretation of data prescribed by these regulations is highly sensitive to minor variations in input, such that near-identical driving patterns may be regarded both as lawful and as unlawful. We then show that the content of the regulation may be represented in monadic second order logic, but argue that a more computationally tame fragment would be preferable for applications. As a case study we consider its representation in linear temporal logic, but show that a representation of the legislation requires formulas of unfeasible complexity, if at all possible.