Formal Verification, Engineering and Business Value
This tackles practical challenges in making formal verification accessible and economically viable for software engineering in embedded systems, but it appears incremental as it builds on existing technologies and tools.
The work addresses applying automated verification technologies like model checking and static analysis to large-scale embedded C/C++ code, packaging them for developers without formal verification background, and convincing businesses to pay for such tools, based on experience with the Goanna source code analyzer.
How to apply automated verification technology such as model checking and static program analysis to millions of lines of embedded C/C++ code? How to package this technology in a way that it can be used by software developers and engineers, who might have no background in formal verification? And how to convince business managers to actually pay for such a software? This work addresses a number of those questions. Based on our own experience on developing and distributing the Goanna source code analyzer for detecting software bugs and security vulnerabilities in C/C++ code, we explain the underlying technology of model checking, static analysis and SMT solving, steps involved in creating industrial-proof tools.