Boolean Algebra of Shape Analysis Constraints
Lecture notes in computer sciencePublished 1 January 2004Open access
Viktor Kunčak, Martin Rinard
Citations15
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 family of formulas in (classical, two-valued) logic that are isomorphic to three-valued structures and represent the same sets of concrete states are introduced.
Abstract
LARA
Keywords
Computer ScienceEngineering
Lecture notes in computer scienceConstruction of abstract state graphs with PVS
1,471 Citations1997Susanne Graf, Hassen Saı̈di
This paper proposes a method for the automatic construction of an abstract state graph of an arbitrary system using the Pvs theorem prover.
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.
ACM Transactions on Programming Languages and SystemsParametric shape analysis via 3-valued logic
784 Citations2002Mooly Sagiv, Thomas Reps +1 more
A parametric framework for shape analysis that can be instantiated in different ways to create different shape-analysis algorithms that provide varying degrees of efficiency and precision is presented.
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.
ACM SIGPLAN NoticesA static analyzer for large safety-critical software
577 Citations2003Bruno Blanchet, Patrick Cousot +6 more
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.
ACM SIGPLAN NoticesBI as an assertion language for mutable data structures
499 Citations2011Samin Ishtiaq, Peter W. O’Hearn
A model in which the law of the excluded middle holds is given, thus showing that the approach to logic BI of bunched implications of O'Hearn and Pym is compatible with classical logic.
ACM SIGPLAN NoticesAnalysis of pointers and structures
432 Citations2004David Chase, Mark N. Wegman +1 more
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.
Refinement Calculus
423 Citations1998Ralph‐Johan Back, Joakim Wright
Categories The authors can generalize the notion of a concrete category to an (abstract) category, where the sets with structure are the objects and the structure-preserving functions are the morphisms of the abstract category.
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.
Interprocedural may-alias analysis for pointers
326 Citations1994Alain Deutsch
A new parametric framework for analyzing recursive pointer data structures is presented which can express a new natural class of alias information not accessible to existing methods, and which on numerous examples that occur in practice is much more precise than recently published algorithms.
ACM Transactions on Programming Languages and SystemsSolving shape-analysis problems in languages with destructive updating
324 Citations1998Mooly Sagiv, Thomas Reps +1 more
An algorithm is given that uses finite shape graphs to approximate conservatively the possible “shapes” that heap-allocated structures in a program can take on, and is sometimes able to show that when the input to the program is a circular list, the output is also a circular lists.
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.
Is it a tree, a DAG, or a cyclic graph? A shape analysis for heap-directed pointers in C
284 Citations1996Rakesh Ghiya, Laurie Hendren
The design and implementation of a practical shape analysis for C to aid in the disambiguation of heap-allocated data structures by estimating the shape of the data structure accessible from each heap-directed pointer is reported on.
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.
The pointer assertion logic engine
264 Citations2001Anders Møller, Michael I. Schwartzbach
A new framework for verifying partial specifications of programs in order to catch type and memory errors and check data structure invariants and can verify a large class of data structures, namely all those that can be expressed as graph types.
ACM SIGPLAN NoticesDetecting conflicts between structure accesses
214 Citations1988James R. Larus, Paul Hilfinger
A flexible approach to interprocedural data flow analysis and programs with recursive data structures
211 Citations1982Neil D. Jones, Steven S. Muchnick
A new approach to data flow analysis of procedural programs and programs with recursive data structures is described, which depends on simulation of the interpreter for the subject programming language using a retrieval function to approximate a program's data structures.
Lecture notes in computer scienceAlias Types
210 Citations2000Frederick Smith, David Walker +1 more
This work presents a new typed language that allows functions to specify the shape of the store that they expect and to track the flow of pointers through a computation, and is expressive enough to represent pointer aliasing and yet safely permit destructive operations.
Lecture notes in computer scienceSymbolic Implementation of the Best Transformer
155 Citations2004Thomas Reps, Mooly Sagiv +1 more
This paper shows how to achieve, under certain conditions, abstract-interpretation algorithms that enjoy the best possible precision for a given abstraction.
Detecting conflicts between structure accesses
153 Citations1988James R. Larus, Paul Hilfinger
This paper describes a dataflow computation that produces a conservative description of the aliases visible at any point in a program that shows how alias graphs can be used to detect potential conflicts.
Points-to analysis using BDDs
141 Citations2003Marc Berndl, Ondřej Lhoták +3 more
This paper reports on a new approach to solving a subset-based points-to analysis for Java using Binary Decision Diagrams (BDDs), and introduces BDDs and operations on BDDs using some simple points-to examples.
Role analysis
127 Citations2002Viktor Kunčak, Patrick Lam +1 more
An interprocedural, compositional, and context-sensitive role analysis algorithm that verifies that a program maintains role constraints is presented.
Putting static analysis to work for verification
117 Citations2000Tal Lev-Ami, Thomas Reps +2 more
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.
Shape types
99 Citations1997Pascal Fradet, Daniel Le Métayer
This work provides a syntax for a smooth integration of shape types defined as context-free graph grammars, and defines graphs in set-theoretic terms, and graph modifications as multiset rewrite rules.
Lecture notes in computer scienceRelative Completeness of Abstraction Refinement for Software Model Checking
97 Citations2002Thomas Ball, Andreas Podelski +1 more
It is shown that whenever backward fixpoint iteration with oracle-guided widening succeeds in proving a property ?
A general data dependence test for dynamic, pointer-based data structures
96 Citations1994Joseph Hummel, Laurie Hendren +1 more
This paper presents a new technique for performing more accurate data dependence testing in the presence of dynamic, pointer-based data structures, and demonstrates its effectiveness by breaking false dependences that existing approaches cannot, and provides results which show that removing these dependences enables significant parallelization of a real application.
Lecture notes in computer scienceSymbolically Computing Most-Precise Abstract Operations for Shape Analysis
95 Citations2004G. Yorsh, Thomas Reps +1 more
This paper presents a new algorithm that takes as input an abstract value and a precondition p, and computes the most-precise abstract value for the stores in X that satisfy p.
UNO: Static Source Code Checking for User-Defined Properties 1
80 Citations2002Gerard J. Holzmann, Murray Hill
A simple source code analyzer, U NO, that tries to remedy the problems of typical static analysis tools, and can be extended by the user with the definition of applicationdependent properties, which are written as ANSI-C functions.
Lecture notes in computer scienceA Decidable Logic for Describing Linked Data Structures
69 Citations1999Michael Benedikt, Thomas Reps +1 more
It is shown that Lr is decidable, and it is explained how Lr relates to two previously defined structuredescription formalisms by showing how an arbitrary shape descriptor from each of these formalisms can be translated into an Lr formula.
Lecture notes in computer scienceInterprocedural Shape Analysis for Recursive Programs
68 Citations2001Noam Rinetzky, Mooly Sagiv
A novel technique for shape analysis of recursive programs that can verify the absence of memory leaks in many recursive programs; this is beyond the capabilities of existing algorithms.
Lecture notes in computer scienceFinite Differencing of Logical Formulas for Static Analysis
59 Citations2003Thomas Reps, Mooly Sagiv +1 more
Lecture notes in computer scienceA Trace Model for Pointers and Objects
51 Citations1999C. A. R. Hoare, He Jifeng
A mathematical model and language for the formulation of assertions about objects and pointers are introduced, and a graphical calculus may help in reasoning about program correctness, which deals with both garbage-collected heaps and the other kind.
Lecture notes in computer scienceMONA Implementation Secrets
43 Citations2001Nils Klarlund, Anders Møller +1 more
Storeless semantics and alias logic
38 Citations2003Marius Bozga, Radu Iosif +1 more
This work explores the principles of storeless semantics from a logical point of view, first defining a simple logic to completely characterize heap structures up to isomorphism and extending it to a full-blown alias logic that allows to express regular properties of unbounded heap structures.
Lecture notes in computer scienceCompactly Representing First-Order Structures for Static Analysis
28 Citations2002Roman Manevich, G. Ramalingam +3 more
This paper describes and evaluates two novel structure representation techniques and shows that both the OBDD and functional implementations reduce space consumption in TVLA by a factor of 4 to 10 relative to the current TVLA state representation, without compromising analysis time.
Lecture notes in computer scienceShape Analysis through Predicate Abstraction and Model Checking
23 Citations2002Dennis Dams, Kedar S. Namjoshi
A new framework, based on predicate abstraction and model checking, is proposed for shape analysis of programs, which results in a predicate-discovery procedure that identifies predicates relevant for correctness, using an analysis based on weakest preconditions, and creates a finite state abstract program.
Existential heap abstraction entailment is undecidable
18 Citations2003Viktor Kunčak, Martin Rinard
Lecture notes in computer scienceClass-Level Modular Analysis for Object Oriented Languages
17 Citations2003Francesco Logozzo
This paper addresses the problem of performing a class static analysis in a modular fashion, i.e. by just analyzing the class code and not the full program, and shows how to discover, in a fully automatic way, a class invariant.
Lecture notes in computer scienceBoolean Algebra of Shape Analysis Constraints
15 Citations2004Viktor Kunčak, Martin Rinard
A family of formulas in (classical, two-valued) logic that are isomorphic to three-valued structures and represent the same sets of concrete states are introduced.
arXiv (Cornell University)Logical Characterizations of Heap Abstractions
14 Citations2003G. Yorsh, Thomas Reps +2 more
Information Processing LettersKleene's Logic with Equality
11 Citations2001Flemming Nielson, Hanne Riis Nielson +1 more
It follows that the so-called summary predicate, considered in previous applications of Kleene's Logic for static analysis of programs, can be derived from equality; this leads to a substantial simplification in the notion of approximation between structures.
Lecture notes in computer scienceExistential Heap Abstraction Entailment Is Undecidable
9 Citations2003Viktor Kunčak, Martin Rinard
It is argued that heap specification languages should avoid second-order existential quantification in favor of explicitly specifying a criterion for summarizingObjects, because the satisfiability of regular graph constraints is decidable.
arXiv (Cornell University)Typestate Checking and Regular Graph Constraints
7 Citations2004Viktor Kunčak, Martin Rinard
The undecidability of implication of regular graph constraints implies that there is no algorithm that will verify that procedure preconditions are met or that the invariants are maintained when these properties are expressed in any specification language at least as expressive asregular graph constraints.
On the Boolean Algebra of Shape Analysis Constraints
5 Citations2003Viktor Kunčak, Martin Rinard
arXiv (Cornell University)Roles Are Really Great!
4 Citations2004Viktor Kunčak, Patrick Lam +1 more
A new role system for specifying changing referencing relationships of heap objects and an interprocedural, compositional, and context-sensitive role analysis algorithm that verifies that a program respects the role constraints.
Lecture notes in computer scienceA Language for Role Specifications
3 Citations2003Viktor Kunčak, Patrick Lam +1 more
A programming model which allows the developer to specify the roles of objects at different points in the computation and the effect of each operation at the granularity of role changes that occur in identified regions of the heap is provided.