Formally-verified static analyzers and compilers
In its quest for software perfection, the critical software industry has been progressively embracing the use of formal verification tools (static analyzers, program provers, model checkers) as a complement, or even as an alternative, to traditional software validation techniques based on testing and reviews. The usefulness of verification tools in the certification of critical software is, however, limited by the amount of trust one can have in their results. Two major risks exist: unsoundness of verification tools (failing to detect a misbehaving program) and miscompilation (post-verification introduction of bugs during the production of executable code). The Verasco project investigates a radical, mathematically-grounded solution to these issues: the formal verification of compilers and verification tools themselves.

Number of scientific articles published: 0

Number of patents filed: 0

Number of product’s innovation: 0

Number of product’s innovation service: 0

Number of projected jobs created: 0

Number of jobs maintained: 0

Number of related companies creation: 0