Verified squared: does critical software deserve verified tools?

Abstract

The formal verification of programs has progressed tremendously in the last decade. In this talk, I review some of the obstacles that [6, 8, 15, 18] remain to be lifted before source-level verification tools can be taken really seriously in the critical software industry. A direction I advocate is the systematic formal verification of the development tools that participate in the production and verification of critical software.