Skip to main content

Formal verification, engineering and business value


Ralf Huuck

NICTA, Sydney, Australia
UNSW, Australia


How to apply automated verification technology such as model checking and static program analy- sis 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 veri- fication? 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, and we share some expected as well as unexpected application results.

BibTeX Entry

    author           = {Huuck, Ralf},
    month            = dec,
    year             = {2012},
    keywords         = {formal methods, engineering, business, position paper },
    address          = {Kyoto, Japan},
    title            = {Formal Verification, Engineering and Business Value},
    pages            = {1--4},
    booktitle        = {Formal Techniques for Safety-Critical Systems},
    paperurl         = {},
    publisher        = {EPTCS}


Served by Apache on Linux on seL4.