Skip to main content

Formal verification, engineering and business value

Authors

Ralf Huuck

NICTA, Sydney, Australia
UNSW, Australia

Abstract

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

  @inproceedings{Huuck_12,
    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},
    publisher        = {EPTCS}
  }

Download

Served by Apache on Linux on seL4.