Automatic predicate abstraction of C programs
Published 1 May 2001
Thomas Ball, Rupak Majumdar, Todd Millstein, Sriram K. Rajamani
Citations432
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 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.
Abstract
Model checking has been widely successful in validating and debugging designs in the hardware and protocol domains. However, state-space explosion limits the applicability of model checking tools, so model checkers typically operate on abstractions of systems.
Keywords
Computer Science
IEEE Transactions on ComputersGraph-Based Algorithms for Boolean Function Manipulation
8,829 Citations1986Bryant
Experimental results from applying a new data structure for representing Boolean functions and an associated set of manipulation algorithms to problems in logic design verification demonstrate the practicality of this approach.
Abstract interpretation
6,131 Citations1977Patrick Cousot, Radhia Cousot
Proof-carrying code
1,807 Citations1997George C. Necula
It is shown in this paper how proof-carrying code might be used to develop safe assembly-language extensions of ML programs and the adequacy of concrete representations for the safety policy, the safety proofs, and the proof validation is proved.
Precise interprocedural dataflow analysis via graph reachability
1,135 Citations1995Thomas Reps, Susan Horwitz +1 more
The paper shows how a large class of interprocedural dataflow-analysis problems can be solved precisely in polynomial time by transforming them into a special kind of graph-reachability problem.
IEEE Transactions on Software EngineeringProving the Correctness of Multiprocess Programs
1,101 Citations1977Leslie Lamport
The inductive assertion method is generalized to permit formal, machine-verifiable proofs of correctness for multiprocess programs, represented by ordinary flowcharts, and no special synchronization mechanisms are assumed.
Enforcing high-level protocols in low-level software
487 Citations2001Robert DeLine, Manuel Fähndrich
The utility of this approach is validated by enforcing protocols present in the interface between the Windows 2000 kernel and its device drivers, which enforces statically that resources cannot be leaked.
Parametric shape analysis via 3-valued logic
337 Citations1999Mooly Sagiv, Thomas Reps +1 more
A family of abstract-interpretation algorithms that are capable of determining "shape invariants" of programs that perform destructive updating on dynamically allocated storage by varying the vocabulary used in the three-valued logic.
Unification-based pointer analysis with directional assignments
300 Citations2000Manuvir Das
This algorithm provides a method for obtaining precise flow-insensitive points-to information for large C programs and lies between Steensgaard's algorithm and Andersen's algorithm in terms of both precision and running time.
BI as an assertion language for mutable data structures
281 Citations2001Samin Ishtiaq, Peter W. O’Hearn
A model in which the law of the excluded middleholds is given is given, thus showing that the approach is compatible with classical logic, and a local character enjoyed by specifications in the logic is described, which enables a class of frame axioms, which say what parts of the heap don't change, to be inferred automatically.
Set-based analysis of ML programs
209 Citations1994Nevin Heintze
This paper develops an approximate “set-based” operational semantics for the language, which formalizes the intuition of treating program variables as sets and develops an O(n3) algorithm for computing the set based approximation of a program.
Interprocedural modification side effect analysis with pointer aliasing
153 Citations1993William Landi, Barbara G. Ryder +1 more
Improving data-flow analysis with path profiles
130 Citations1998Glenn Ammons, James R. Larus
Tool-supported program abstraction for finite-state verification
128 Citations2001Matthew B. Dwyer, John Hatcliff +5 more
Implementation of an array bound checker
109 Citations1977Norihisa Suzuki, Kiyoshi Ishihata
This paper describes a system which checks correctness of array accesses automatically without any inductive assertions or human interaction and creates logical assertions immediately before array elements such that these assertions must be true whenever the control passes the assertion in order for the access to be valid.
Path-sensitive value-flow analysis
77 Citations1998Rastisalv Bodík, Sadun Anik
A data-flow analysis framework that overcomes the problem of naming the value that flows between equivalent computations with different lexical names by synthesizing a name space tailored for tracing the values whose flow is of interest to a given data- flow problem is presented.
Safety checking of machine code
73 Citations2000Zhichen Xu, Barton P. Miller +1 more
The safety checker was able to either prove that an example met the necessary safety conditions, or identify the places where the safety conditions were violated, and the checking times ranged from less than a second to 14 seconds on an UltraSPARC machine.
Lecture notes in computer scienceParameterized Verification of Multithreaded Software Libraries
61 Citations2001Thomas Ball, Sagar Chaki +1 more
It is demonstrated the expressiveness of LGFSMs as models, and the effectiveness of Beacon as a model checking tool by modeling a multithreaded memory manager Rockall developed at Microsoft Research as an LGFSM, and using Beacon to check a critical safety property of Rockall.
A General Axiom of Assignment
57 Citations1982Joseph M. Morris
The goal is to make manageable the formal verification of list-processing programs, using axiomatic semantics, which is more systematic than previous treatments, and is more general.
Information Processing LettersAnnotation inference for modular checkers
54 Citations2001Cormac Flanagan, Rajeev Joshi +1 more
A general approach to annotation inference for a given static program checker that reuses the checker as a subroutine is presented and shows how it applies to ESC.