USP Electronic Research Repository

High performance static analysis for industry

Bradley, M. and Cassez, F. and Fehnker, Ansgar and Given-Wilson, T. and Huuck, R. (2012) High performance static analysis for industry. Electronic Notes in Theoretical Computer Science, 289 . pp. 3-14. ISSN 1571-0661

[img] PDF - Accepted Version
Restricted to Registered users only

Download (435Kb)


    Static source code analysis for software bug detection has come a long way since its early beginnings as a compiler technology. The introduction of new technologies and tools based on new theoretical results has drastically changed static analysis. 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.

    Item Type: Journal Article
    Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
    Divisions: Faculty of Science, Technology and Environment (FSTE) > School of Computing, Information and Mathematical Sciences
    Depositing User: Ansgar Fehnker
    Date Deposited: 01 May 2013 15:07
    Last Modified: 11 Jul 2016 15:42

    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...