Looking for a software bug definition and the definition of the way to solve it: definition of formal verification

Public Certification of Third-Party Specification and software We are a body who can do
Public Certification of Specification and Software according to the (4+1)-tuple (Σ, Π, ∆, Λ, Φ) method

Our commitment with formal verification implies a strong concern about the verification of the Coq extraction mechanism itself. The MetaCoq project aims to do exactly that, with horizon 2022 for having a first prototype.

In this article we analyse the not solved problem of the time span calculation in classic calendars, and how the problems come bigger in UTC calendars. And their consequences.

Our work in the transportation law field has given us perspective on the kind of problems that need to be solved to develop 100-reliable software for Law applications.

A logical and computational analysis of European transport regulations