Our CTO Benjamin Monate giving a talk at the Sound Static Analysis for Security Workshop 2018 at the National Institute for Standards & Technology (NIST).
Applying formal methods to existing software: what can you expect?
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, Monate discussed 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.