Static source code analysis for software bug detection has come a long way since its early beginnings as a compiler technology. However, with the introduction of more sophisticated algorithmic techniques, such as model checking and constraint solving, questions about performance are a major concern. In this work we present an empirical study of our industrial strength source code analysis tool Goanna that uses a model checking core for static analysis of C/C++ code. We present the core technology and abstraction mechanism with a focus on performance, as guided by experience from having analyzed millions of lines of code. In particular, we present results from our recent study within the NIST/DHS SAMATE program. The results show that, maybe surprisingly, formal verification techniques can be used successfully in practical industry applications scaling roughly linearly, even for millions of lines of code.
|Number of pages||12|
|Journal||Electronic proceedings in theoretical computer science|
|Publication status||Published - 2012|
Bradley, M., Cassez, F., Fehnker, A., Given-Wilson, T., & Huuck, R. (2012). High Performance Static Analysis for Industry. Electronic proceedings in theoretical computer science, 289, 3-14. https://doi.org/10.1016/j.entcs.2012.11.002