public Certification of a Specification and
its Software (PCSS)
its Software (PCSS)
We guarantee the mathematical correctness of your
specification and its exact transmission to the
final code.
final code.
It is not possible to establish a proven equivalence among
formal specification and natural language, nor even to any
intermediate abstraction level of mathematical language.
Those worlds are disconnected.
We also have the issue that a sentence in natural language
can be interpreted in different ways: natural language is
ambiguous. Knowing that, there are chances to find solutions.
~ Guillermo Errezil
(Director)
(Director)
Our philosophy
If we want to create perfect software, we would not write a single line of code ,
just focus on technical and formal specifications.
The code is obtained
by the formally verified extraction mechanism
In accordance with this choice, we are committed members of the Coq
Community and we contribute new features to both Coq and MathComp.
We have a method to create the most secure software ever invented.