Model Checking Software at Compile Time

Ansgar Fehnker, Ralf Huuck, Patrick Jayet, Michel Lussenburg, Felix Rauch

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

27 Citations (Scopus)

Abstract

Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analysis. Those approaches are typically complementary. In this paper we use a model checking approach to solve static analysis problems. This not only avoids the scalability and abstraction issues typically associated with model checking, it allows for specifying new properties in a concise and elegant way, scales well to large code bases, and the built-in optimizations of modern model checkers enable scalability also in terms of numbers of properties to be checked. In particular, we present Goanna, the first C/C++ static source code analyzer using the off-the-shelfmodel checker NuSMV, and we demonstrate Goanna's suitability for developer machines by evaluating its run-time performance, memory consumption and scalability using the source code of OpenSSL as a test bed.
Original languageEnglish
Title of host publicationFirst Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE 2007
PublisherIEEE Computer Society
Pages45-56
Number of pages12
ISBN (Print) 978-0-7695-2856-4
DOIs
Publication statusPublished - 2007
Externally publishedYes
EventFirst Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering 2007 - Shanghai, China
Duration: 6 Jun 20078 Jun 2008
Conference number: 1

Conference

ConferenceFirst Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering 2007
Abbreviated titleTASE 2007
CountryChina
CityShanghai
Period6/06/078/06/08

Fingerprint

Model checking
Scalability
Static analysis
Data storage equipment

Cite this

Fehnker, A., Huuck, R., Jayet, P., Lussenburg, M., & Rauch, F. (2007). Model Checking Software at Compile Time. In First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE 2007 (pp. 45-56). IEEE Computer Society. https://doi.org/10.1109/TASE.2007.34
Fehnker, Ansgar ; Huuck, Ralf ; Jayet, Patrick ; Lussenburg, Michel ; Rauch, Felix. / Model Checking Software at Compile Time. First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE 2007. IEEE Computer Society, 2007. pp. 45-56
@inproceedings{6ec784188327402084537e57a61fb0b4,
title = "Model Checking Software at Compile Time",
abstract = "Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analysis. Those approaches are typically complementary. In this paper we use a model checking approach to solve static analysis problems. This not only avoids the scalability and abstraction issues typically associated with model checking, it allows for specifying new properties in a concise and elegant way, scales well to large code bases, and the built-in optimizations of modern model checkers enable scalability also in terms of numbers of properties to be checked. In particular, we present Goanna, the first C/C++ static source code analyzer using the off-the-shelfmodel checker NuSMV, and we demonstrate Goanna's suitability for developer machines by evaluating its run-time performance, memory consumption and scalability using the source code of OpenSSL as a test bed.",
author = "Ansgar Fehnker and Ralf Huuck and Patrick Jayet and Michel Lussenburg and Felix Rauch",
year = "2007",
doi = "10.1109/TASE.2007.34",
language = "English",
isbn = "978-0-7695-2856-4",
pages = "45--56",
booktitle = "First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE 2007",
publisher = "IEEE Computer Society",
address = "United States",

}

Fehnker, A, Huuck, R, Jayet, P, Lussenburg, M & Rauch, F 2007, Model Checking Software at Compile Time. in First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE 2007. IEEE Computer Society, pp. 45-56, First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering 2007, Shanghai, China, 6/06/07. https://doi.org/10.1109/TASE.2007.34

Model Checking Software at Compile Time. / Fehnker, Ansgar; Huuck, Ralf; Jayet, Patrick; Lussenburg, Michel; Rauch, Felix.

First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE 2007. IEEE Computer Society, 2007. p. 45-56.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Model Checking Software at Compile Time

AU - Fehnker, Ansgar

AU - Huuck, Ralf

AU - Jayet, Patrick

AU - Lussenburg, Michel

AU - Rauch, Felix

PY - 2007

Y1 - 2007

N2 - Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analysis. Those approaches are typically complementary. In this paper we use a model checking approach to solve static analysis problems. This not only avoids the scalability and abstraction issues typically associated with model checking, it allows for specifying new properties in a concise and elegant way, scales well to large code bases, and the built-in optimizations of modern model checkers enable scalability also in terms of numbers of properties to be checked. In particular, we present Goanna, the first C/C++ static source code analyzer using the off-the-shelfmodel checker NuSMV, and we demonstrate Goanna's suitability for developer machines by evaluating its run-time performance, memory consumption and scalability using the source code of OpenSSL as a test bed.

AB - Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analysis. Those approaches are typically complementary. In this paper we use a model checking approach to solve static analysis problems. This not only avoids the scalability and abstraction issues typically associated with model checking, it allows for specifying new properties in a concise and elegant way, scales well to large code bases, and the built-in optimizations of modern model checkers enable scalability also in terms of numbers of properties to be checked. In particular, we present Goanna, the first C/C++ static source code analyzer using the off-the-shelfmodel checker NuSMV, and we demonstrate Goanna's suitability for developer machines by evaluating its run-time performance, memory consumption and scalability using the source code of OpenSSL as a test bed.

U2 - 10.1109/TASE.2007.34

DO - 10.1109/TASE.2007.34

M3 - Conference contribution

SN - 978-0-7695-2856-4

SP - 45

EP - 56

BT - First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE 2007

PB - IEEE Computer Society

ER -

Fehnker A, Huuck R, Jayet P, Lussenburg M, Rauch F. Model Checking Software at Compile Time. In First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE 2007. IEEE Computer Society. 2007. p. 45-56 https://doi.org/10.1109/TASE.2007.34