High Performance Static Analysis for Industry

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

Research output: Contribution to journalArticleAcademicpeer-review

8 Citations (Scopus)
7 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.
Original languageEnglish
Pages (from-to)3-14
Number of pages12
JournalElectronic proceedings in theoretical computer science
Volume289
DOIs
Publication statusPublished - 2012
Externally publishedYes

Fingerprint

Model checking
Static analysis
Industry
Formal verification

Cite this

Bradley, Mark ; Cassez, Franck ; Fehnker, Ansgar ; Given-Wilson, Thomas ; Huuck, Ralf. / High Performance Static Analysis for Industry. In: Electronic proceedings in theoretical computer science. 2012 ; Vol. 289. pp. 3-14.
@article{7f8e2253d939408d945ff84a8e198c9b,
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.",
author = "Mark Bradley and Franck Cassez and Ansgar Fehnker and Thomas Given-Wilson and Ralf Huuck",
year = "2012",
doi = "10.1016/j.entcs.2012.11.002",
language = "English",
volume = "289",
pages = "3--14",
journal = "Electronic proceedings in theoretical computer science",
issn = "2075-2180",
publisher = "Open Publishing Association",

}

High Performance Static Analysis for Industry. / Bradley, Mark; Cassez, Franck; Fehnker, Ansgar; Given-Wilson, Thomas; Huuck, Ralf.

In: Electronic proceedings in theoretical computer science, Vol. 289, 2012, p. 3-14.

Research output: Contribution to journalArticleAcademicpeer-review

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

PY - 2012

Y1 - 2012

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.

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.

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 proceedings in theoretical computer science

JF - Electronic proceedings in theoretical computer science

SN - 2075-2180

ER -