# Formal Verification, Engineering and Business Value

**Authors:** Ralf Huuck  
**arXiv:** [1301.0037](https://arxiv.org/abs/1301.0037)  
**Date:** 2013-01-01  
**Summary page:** https://www.summarizepaper.com/fr/paper/1301.0037v1/

## Abstract

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.