Putting static analysis to work for verification
Published 1 August 2000Open access
Tal Lev-Ami, Thomas Reps, Mooly Sagiv, Reinhard Wilhelm
Citations117
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
A method for finding bugs in code whose models represent all execution traces that involve at most j heap cells and k loop iterations is presented.
Abstract
A method for finding bugs in code is presented. For given small numbers j and k, the code of a procedure is translated into a rela-tional formula whose models represent all execution traces that involve at most j heap cells and k loop iterations. This formula is conjoined with the negation of the procedure's specification. The models of the resulting formula, obtained using a constraint solver, are counterexamples: executions of the code that violate the specification.
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.
Communications of the ACMAn axiomatic basis for computer programming
3,886 Citations1969C. A. R. Hoare
An attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of mathematics by elucidation of sets of axioms and rules of inference.
Lecture notes in computer scienceSymbolic model checking
2,843 Citations1996Emma L. Clarke, K. McMillan +2 more
Using symbolic model checking techniques it is possible to verify industrial-size finite state systems and models with more than 10120 states have been verified using special techniques.
Symbolic Model Checking
1,645 Citations1993Kenneth L. McMillan
The symbolic model checking technique revealed subtle errors in this protocol, resulting from complex execution sequences that would occur with very low probability in random simulation runs, and an alternative method is developed for avoiding the state explosion in the case of asynchronous control circuits.
Systematic design of program analysis frameworks
1,598 Citations1979Patrick Cousot, Radhia Cousot
The systematic and correct design of program analysis frameworks with respect to a formal semantics is devoted to the main elements of the lattice theoretic approach to approximate semantic analysis of programs.
The Science of Programming
1,430 Citations1981David Gries
Describes basic programming principles and their step-by- step applications and shows how to apply them to real-world problems.
Points-to analysis in almost linear time
1,074 Citations1996Bjarne Steensgaard
This is the asymptotically fastest non-trivial interprocedural points-to analysis algorithm yet described and is based on a non-standard type system for describing a universally valid storage shape graph for a program in linear space.
Art of Software Testing
566 Citations1979Glenford J. Myers
ACM SIGPLAN NoticesAnalysis of pointers and structures
432 Citations2004David Chase, Mark N. Wegman +1 more
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.
Analysis of pointers and structures
297 Citations1990David Chase, Mark N. Wegman +1 more
This work follows that of Jones and Muchnick [Jbl81] who summarize the data structures allocated in a heap by making a graph, in which one node corresponds to possibly many nodes in the heap, and views the program as a generator for data structures.
Lecture notes in computer scienceTVLA: A System for Implementing Static Analyses
250 Citations2000Tal Lev-Ami, Mooly Sagiv
TVLA has been implemented in Java and was successfully used to perform shape analysis on programs manipulating linked data structures, to prove safety properties of Mobile Ambients, and to verify the partial correctness of several sorting programs.
Data flow analysis for verifying properties of concurrent programs
189 Citations1994Matthew B. Dwyer, Lori A. Clarke
An approach, based on data flow analysis, that can provide cost-effective analysis of concurrent programs with respect to explicitly stated correctness properties and implemented a prototype toolset that automates the analysis for programs with explicit tasking and rendezvous style communication.
International Journal of Parallel ProgrammingRecursive data structures
169 Citations1975C. A. R. Hoare
A pleasing notation by which treelike data structures can be declared and processed is suggested; it gives the axioms which specify their properties, and an efficient implementation method is suggested.
Abstract debugging of higher-order imperative languages
145 Citations1993François Bourdoncle
It is shown how invariant assertions and intermittent assertions, such as termination, can be used to formally debug programs and how abstract debugging can be effectively and efficiently applied to higher-order imperative programs with exceptions and jumps to non-local labels.
Communications of the ACMThe synthesis of loop predicates
136 Citations1974Ben Wegbreit
Two classes of techniques are considered: heuristic methods which derive loop predicates from boundary conditions and/or partially specified inductive assertions and extraction methods which use input predicates and appropriate weak interpretations to obtain certain classes of loop predicate by an evaluation on the weak interpretation.
IEEE Transactions on Software EngineeringCecil: a sequencing constraint language for automatic static analysis generation
119 Citations1990K. Olender, Leon J. Osterweil
A flexible and general mechanism for specifying problems relating to the sequencing of events and mechanically translating them into dataflow analysis algorithms capable of solving those problems is presented.
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.
IEEE Transactions on Software EngineeringSymbolic Evaluation and the Analysis of Programs
106 Citations1979Thomas E. Cheatham, Glenn Holloway +1 more
A symbolic evaluator uses conditional expressions to represent the uncertainty that arises from branching and develops and attempts to solve recurrence relations that describe the behavior of loop variables.
Automatic verification of pointer programs using monadic second-order logic
87 Citations1997Jakob L. Jensen, Michael E. Jørgensen +2 more
A technique for automatic verification of pointer programs based on a decision procedure for the monadic second-order logic on finite strings that can be used to verify extensive properties of smaller pointer programs and could be particularly useful in a teaching environment.
Lecture notes in computer scienceChecking Cleanness in Linked Lists
63 Citations2000Nurit Dor, Michael Rodeh +1 more
A new algorithm is presented that automatically uncovers memory errors such as NULL pointers dereference and memory leaks in C programs and yields more accurate results, does not report any false alarm and usually runs even faster and consumes less space than a less precise algorithm.
ACM Transactions on Software Engineering and MethodologyInterprocedural static analysis of sequencing constraints
55 Citations1992K. Olender, Leon J. Osterweil
The algorithms used for interprocedural analysis are described, the problems arising from the analysis of real-world programs are related, and how these difficulties were overcome are shown.
ACM Transactions on Software Engineering and MethodologyUsing shape analysis to reduce finite-state models of concurrent Java programs
37 Citations2000James C. Corbett
This article shows how shape analysis can be used to greatly reduce the size of finite-state models of concurrent Java programs by determining which heap-allocated variables are accessible only by a single thread, and which shared variables are protected by locks.
Assignment and Linked Data Structures
19 Citations1982Joseph M. Morris
This paper discusses the axiom of assignment when the assignment is to a pointer field of a node, and the postcondition is a connectivity relation.
IEEE Transactions on Software EngineeringADI: Automatic Derivation of Invariants
12 Citations1980Merana Tamir
This paper describes an interactive computer program, called ADI, which automatically generates the needed inductive assertions and is also able to extend partial loop assertions supplied by the user to form complete assertions.