loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07)
Model Checking Software at Compile Time
Shanghai, China
June 06-June 08
ISBN: 0-7695-2856-2
Ansgar Fehnker, University of New South Wales, Australia
Ralf Huuck, University of New South Wales, Australia
Patrick Jayet, University of New South Wales, Australia
Michel Lussenburg, University of New South Wales, Australia
Felix Rauch, University of New South Wales, Australia
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.
Citation:
Ansgar Fehnker, Ralf Huuck, Patrick Jayet, Michel Lussenburg, Felix Rauch, "Model Checking Software at Compile Time," tase, pp.45-56, First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07), 2007
Usage of this product signifies your acceptance of the Terms of Use.