Static Analysis versus Software Model Checking for Bug Finding
Lecture notes in computer sciencePublished 1 January 2004
Dawson Engler, Madanlal Musuvathi
Citations120
SJR quartileQ2
SJR score0.35
SNIP0.55
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
This paper describes experiences with software model checking after several years of using static analysis to find errors, finding that expectations were often wrong.
Abstract
This paper describes experiences with software model checking after several years of using static analysis to find errors. We initially thought that the trade-off between the two was clear: static analysis was easy but would mainly find shallow bugs, while model checking would require more work but would be strictly better – it would find more errors, the errors would be deeper, and the approach would be more powerful. These expectations were often wrong.
Keywords
Computer Science
Ad hoc On-Demand Distance Vector (AODV) Routing
10,646 Citations2003Colin Perkins, Elizabeth M. Belding‐Royer +1 more
The Ad hoc On-Demand Distance Vector routing protocol uses destination sequence numbers to ensure loop freedom at all times, avoiding problems (such as "counting to infinity") associated with classical distance vector protocols.
IEEE Transactions on Software EngineeringThe model checker SPIN
3,736 Citations1997Gerard J. Holzmann
An overview of the design and structure of the verifier, its theoretical foundation, and an overview of significant practical applications are given.
Automated Software EngineeringModel Checking Programs
1,353 Citations2003Willem Visser, Klaus Havelund +3 more
A verification and testing environment for Java, called Java PathFinder (JPF), which integrates model checking, program analysis and testing, and uses state compression to handle large states and partial order reduction, slicing, abstraction and run-time analysis techniques to reduce the state space.
Extended static checking for Java
1,339 Citations2002Cormac Flanagan, K. Rustan M. Leino +4 more
The Extended Static Checker for Java (ESC/Java) is introduced, an experimental compile-time program checker that finds common programming errors and provides programmers with a simple annotation language with which programmer design decisions can be expressed formally.
Model checking for programming languages using VeriSoft
823 Citations1997Patrice Godefroid
This paper discusses how model checking can be extended to deal directly with "actual" descriptions of concurrent systems, e.g., implementations of communication protocols written in programming languages such as C or C++, and introduces a new search technique that is suitable for exploring the state spaces of such systems.
Bugs as deviant behavior
747 Citations2001Dawson Engler, David Yu Chen +3 more
Six checkers are developed that extract beliefs by tailoring rule "templates" to a system --- for example, finding all functions that fit the rule template "a must be paired with b."
ACM SIGPLAN NoticesAutomatic predicate abstraction of C programs
703 Citations2012Thomas Ball, Rupak Majumdar +2 more
This work presents the first algorithm to automatically construct a predicate abstraction of programs written in am industrial programming language such as C, and its implementation in a tool -- C2BP, part of the SLAM toolkit.
ESP
544 Citations2002Manuvir Das, Sorin Lerner +1 more
This paper presents a new algorithm for partial program verification that runs in polynomial time and space, and shows that property simulation scales to large programs and is accurate enough to verify meaningful properties.
Defense Technical Information Center (DTIC)Checking system rules using system-specific, programmer-written compiler extensions
543 Citations2000Dawson Engler, Benjamin Chelf +2 more
Software Practice and ExperienceA static analyzer for finding dynamic programming errors
508 Citations2000William R. Bush, Jonathan D. Pincus +1 more
A compile‐time analyzer that detects dynamic errors in large, real‐world programs, and provides valuable contextual information to the programmer who needs to understand and repair the defects.
Automatic predicate abstraction of C programs
432 Citations2001Thomas Ball, Rupak Majumdar +2 more
This work presents the first algorithm to automatically construct a predicate abstraction of programs written in an industrial programming language such as C, and its implementation in a tool — C2BP.
Protocol verification as a hardware design aid
399 Citations2003David L. Dill, Andreas J. Drexler +2 more
MOPS
383 Citations2002Hao Chen, David Wagner
A formal approach for finding bugs in security-relevant software and verifying their absence and experience suggests that this approach will be useful in finding a wide range of security vulnerabilities in large programs efficiently.
A system and language for building system-specific, static analyses
352 Citations2002Seth Hallem, Benjamin Chelf +2 more
A flexible, easy-to-use extension language for specifying analyses and an efficent algorithm for executing these extensions, which believe is an effective framework for deploying new bug-finding analyses quickly and easily.
The Stanford FLASH multiprocessor
270 Citations2002Jeffrey S. Kuskin, David Ofelt +11 more
The architecture of FLASH and MAGIC is presented, and the base cache-coherence and message-passing protocols are discussed, and Latency and occupancy numbers, which are derived from the system-level simulator and the Verilog code, are given.
Software Testing Verification and ReliabilitySoftware model checking: extracting verification models from source code†
167 Citations2001Gerard J. Holzmann, Margaret Smith
It is argued, though, that the method was originally developed to allow for a thorough testing of parts of the software of a new commercial telephone switch also has broad applicability to distributed software systems design in general.
A large-scale testbed for reproducible ad hoc protocol evaluations
161 Citations2003Henrik Lundgren, D. Lundberg +3 more
A mobility metric called virtual mobility is introduced that is based on the measured signal quality instead of the geometric distance between nodes, hence it reflects how a routing protocol actually perceives the network's dynamics.
CMC
124 Citations2002Madanlal Musuvathi, David Y. W. Park +3 more
A new model checker, CMC, which checks C and C++ implementations directly, eliminating the need for a separate abstract description of the system behavior, and reduces missed errors as well as time-wasting false error reports resulting from inconsistencies between the abstract description and the actual implementation.
Verification of FLASH cache coherence protocol by aggregation of distributed transactions
81 Citations1996Seungjoon Park, David L. Dill
This paper presents a method to verify the correctness of protocols and distributed algorithms by comparing a state graph of the implementation with a specification which is a stategraph representing the desired abstract behavior.
Software model checking in practice
63 Citations2002Satish Chandra, Patrice Godefroid +1 more
An application of software model checking to the analysis of a large industrial software product: Lucent Technologies' CDMA call-processing library, where it sets up and manages millions of calls to and from mobile devices everyday.
IFIP advances in information and communication technologyA New Scheme for Memory-Efficient Probabilistic Verification
52 Citations1996Ulrich Stern, David L. Dill
Two probabilistic methods — bitstate hashing and hash compaction — have been proposed in the literature that store much fewer bits for each state but come at the price of some probability that not all reachable states will be explored during the search, and that the verifier may thus produce false positives.
A simple method for extracting models for protocol code
44 Citations2001David Lie, Andy Chou +2 more
ACM SIGPLAN NoticesUsing meta-level compilation to check FLASH protocol code
22 Citations2000Andy Chou, Benjamin Chelf +2 more
A case study in how system implementors can use a new programming methodology, metalevel compilation (MC), to easily check for errors in the code used to manage cache coherence on the FLASH shared memory multiprocessor.
Using meta-level compilation to check FLASH protocol code
16 Citations2000Andy Chou, Benjamin Chelf +2 more
A case study in how system implementors can use a new programming methodology, metalevel compilation (MC), to easily check for errors in the code used to manage cache coherence on the FLASH shared memory multiprocessor.
A simple method for extracting models from protocol code
12 Citations2002David Lie, Andy Chou +2 more
A method for automatically extracting models from low level software implementations based on the use of an extensible compiler system, xg++, to perform the extraction, which increases the effectiveness of model checking since the automatically extracted models are more accurate and faithful to the underlying implementation.
Software model checking in practice
3 Citations2002Satish Chandra, Patrice Godefroid +1 more