Applying formal methods to existing software: what can you expect?

Benjamin Monate - TrustInSoft

Formal methods-based source code verification tools have a very strong promise: mathematically prove that a piece of software is perfect. In some specific economic sectors, new languages have been adopted to help developers build perfect-by-construction software. But the vast majority of software is not perfect-by-construction and experience shows that it comes with tons of bugs. In this talk I will discuss what developers can expect from the application of formal methods-based tools to existing imperfect-by-construction code bases, what they should not expect, and how such tools will help make the software better and better by incrementally reducing its hidden technical debt. This work has been supported by the Core Infrastructure Initiative of the Linux foundation.

Download this presentation

About Benjamin Monate

Benjamin Monate is co-founder and CTO of TrustInSoft, the start-up company industrializing the Frama-C source code analyzing framework. He is the initial inventor of Frama-C and lead its research & development team for almost ten years at the CEA.