« BACK TO PROGRAM
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.