High performance static analysis for industry

Mark Bradley; Franck Cassez; Ansgar Fehnker; Thomas Given-Wilson; Ralf Huuck

doi:10.1016/j.entcs.2012.11.002

High performance static analysis for industry

Mark Bradley^*, Franck Cassez, Ansgar Fehnker, Thomas Given-Wilson, Ralf Huuck

^*Corresponding author for this work

Research output: Contribution to journal › Article

8 Citations (Scopus)

2 Downloads (Pure)

Abstract

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. Crown

Original language	English
Pages (from-to)	3-14
Number of pages	12
Journal	Electronic Notes in Theoretical Computer Science
Volume	289
DOIs	https://doi.org/10.1016/j.entcs.2012.11.002
Publication status	Published - 6 Dec 2012
Externally published	Yes

Bibliographical note

Copyright the Author(s) 2012. Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.

Keywords

C/C++
model checking
SAMATE
static analysis
tools
Validation
verification

Access to Document

10.1016/j.entcs.2012.11.002

Publisher version (open access)Final published version, 370 KBLicence: CC BY-NC-ND

Link to publication in Scopus

Fingerprint Dive into the research topics of 'High performance static analysis for industry'. Together they form a unique fingerprint.

Cite this

Bradley, M., Cassez, F., Fehnker, A., Given-Wilson, T., & Huuck, R. (2012). High performance static analysis for industry. Electronic Notes in Theoretical Computer Science, 289, 3-14. https://doi.org/10.1016/j.entcs.2012.11.002

@article{08487563a8f6465da5a89e263c0afe48,

title = "High performance static analysis for industry",

abstract = "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. Crown",

keywords = "C/C++, model checking, SAMATE, static analysis, tools, Validation, verification",

author = "Mark Bradley and Franck Cassez and Ansgar Fehnker and Thomas Given-Wilson and Ralf Huuck",

note = "Copyright the Author(s) 2012. Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.",

year = "2012",

month = "12",

day = "6",

doi = "10.1016/j.entcs.2012.11.002",

language = "English",

volume = "289",

pages = "3--14",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

}

TY - JOUR

T1 - High performance static analysis for industry

AU - Bradley, Mark

AU - Cassez, Franck

AU - Fehnker, Ansgar

AU - Given-Wilson, Thomas

AU - Huuck, Ralf

N1 - Copyright the Author(s) 2012. Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.

PY - 2012/12/6

Y1 - 2012/12/6

N2 - 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. Crown

AB - 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. Crown

KW - C/C++

KW - model checking

KW - SAMATE

KW - static analysis

KW - tools

KW - Validation

KW - verification

UR - http://www.scopus.com/inward/record.url?scp=84870403868&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2012.11.002

DO - 10.1016/j.entcs.2012.11.002

M3 - Article

VL - 289

SP - 3

EP - 14

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -