We are part of Coq consortium
Our contributions to the Coq verification
ecosystem
ecosystem
An extension of the SSReflect library with functions about sequences
The SSReflect library for sequences (GitHub)
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.
Our team developed this function, together with suffix and prefix, and all the required theorems about them to contribute to the MathComp SSReflect library.
Primitive machine signed integers for Coq
See (GitHub)
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.
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
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.