FTSCS 2012
First International Workshop on Formal Techniques for Safety-Critical Systems

(An ICFEM 2012 Satellite Event)

Kyoto, Japan, November 12, 2012


Ralf Huuck (NICTA, Sydney)

Dr Ralf Huuck is a senior researcher with NICTA, Australia's national computer science research research, he is senior lecturer with the University of New South Wales (UNSW), Sydney, and the CEO and co-Founder of Red Lizard Software, an enterprise delivering software source code analysis solutions. Ralf obtained his PhD in formal methods from the University of Kiel, Germany, and was holding visiting appointments in France, Hong Kong, Australia and Japan.

Formal Verification, Engineering and Business Value

-- Why Analyzing 1 Million lines of C/C++ Code is not Enough

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 talk gives answers to 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.