Shape Analysis through Predicate Abstraction and Model Checking

No abstract is available for this paper.

• Publication year

  2002

• Venue

  International Conference on Verification, Model Checking and Abstract Interpretation

• Publication date

  2002-01-09

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/3-540-36384-X_25
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• The SPIN Model Checker

  2003influential reference
• Relative Completeness of Abstraction Refinement for Software Model Checking

  2002cited by this paper
• Predicate abstraction for software verification

  2002cited by this paper
• Lazy abstraction

  2002cited by this paper
• Automatic verification of parameterized networks of processes

  2001cited by this paper
• Verifying safety properties of concurrent Java programs using 3-valued logic

  2001cited by this paper
• The SLAM Toolkit

  2001cited by this paper
• Incremental Verification by Abstraction

  2001cited by this paper
• Interprocedural Shape Analysis for Recursive Programs

  2001cited by this paper
• Successive approximation of abstract transition relations

  2001cited by this paper
• Automatic predicate abstraction of C programs

  2001cited by this paper
• A decision procedure for an extensional theory of arrays

  2001cited by this paper
• Syntactic Program Transformations for Automatic Abstraction

  2000influential reference
• Proving Pointer Programs in Hoare Logic

  2000cited by this paper
• TVLA: A System for Implementing Static Analyses

  2000cited by this paper
• Counterexample-Guided Abstraction Refinement

  2000cited by this paper
• Parametric shape analysis via 3-valued logic

  1999cited by this paper
• A Decidable Logic for Describing Linked Data Structures

  1999cited by this paper
• Experience with Predicate Abstraction

  1999cited by this paper
• Program Analysis as Model Checking of Abstract Interpretations

  1998cited by this paper
• Construction of Abstract State Graphs with PVS

  1997cited by this paper
• The Model Checker SPIN

  1997cited by this paper
• Automatic verification of pointer programs using monadic second-order logic

  1997cited by this paper
• Graphs and Decidable Transductions Based on Edge Constraints (Extended Abstract)

  1994cited by this paper
• Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation

  1992cited by this paper
• Verifying reachability invariants of linked structures

  1983cited by this paper
• The Science of Programming

  1981cited by this paper
• Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

  1977cited by this paper
• Guarded commands, nondeterminacy and formal derivation of programs

  1975cited by this paper
• A Computing Procedure for Quantification Theory

  1960cited by this paper

• Proofs as Relational Invariants of Synthesized Execution Grammars

  2017cites this paper
• Formal Verification of Temporal Properties for Parametrized Concurrent Programs and Concurrent Data Structures

  2015cites this paper
• Using Predicate-based Model Checker for Verifying E-Commerce Protocols

  2014cites this paper
• Requirement and Result of Verifying the Program Code

  2014cites this paper
• Project Description

  2013cites this paper
• A General Framework for Constraint-Based Static Analyses of Java Bytecode Programs

  2013cites this paper
• Predicate abstraction of Java programs with collections

  2012influential citation
• Reachability analysis of program variables

  2012cites this paper
• Decision procedures for the temporal verification of concurrent data structures

  2011cites this paper
• Juggrnaut: Graph Grammar Abstraction for Unbounded Heap Structures

  2010cites this paper
• Software Verification by Combining Program Analyses of Adjustable Precision

  2010cites this paper
• Verification of Pointer Programs

  2009cites this paper
• Partially disjunctive shape analysis

  2009cites this paper
• Symbolic shape analysis

  2009cites this paper
• Symbolic execution with abstraction

  2009cites this paper
• Verification of recursive methods on tree-like data structures

  2009cites this paper
• MLAT: a tool for heap analysis based on predicate abstraction by modal logic

  2008cites this paper
• Cooperatively combining program verifiers: foundations and tool support

  2008cites this paper
• Verifying Dynamic Pointer-Manipulating Threads

  2008cites this paper
• Abstracting Complex Data Structures by Hyperedge Replacement

  2008cites this paper
• Shape analysis by augmentation, abstraction, and transformation

  2007cites this paper
• Proof Systems for Inductive Reasoning in the Logic of Bunched Implications

  2007cites this paper
• An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures

  2007cites this paper
• Verifying Concurrent List-Manipulating Programs by LTL Model Checking

  2007cites this paper
• Implementing certified programming language tools in dependent type theory

  2007cites this paper
• Array Abstractions from Proofs

  2007cites this paper
• The Spotlight Principle

  2007cites this paper
• Modular data structure verification

  2007cites this paper
• Maintaining Doubly-Linked List Invariants in Shape Analysis with Local Reasoning

  2007cites this paper
• The spotlight principle: on combining process-summarizing state abstractions

  2007cites this paper
• A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs

  2006influential citation
• A Theory of Singly-Linked Lists and its Extensible Decision Procedure

  2006cites this paper
• Lightweight Analysis of Acyclic Unshared Lists

  2006cites this paper
• Local Reasoning for Termination

  2006cites this paper
• Verifying properties of well-founded linked lists

  2006influential citation
• Lazy Shape Analysis

  2006cites this paper
• Symbolic Execution with Abstract Subsumption Checking

  2006cites this paper
• A logic and decision procedure for verification of heap-manipulating programs

  2006cites this paper
• Summary of the Research Done during the Sabbatical Year from Oct . 2005 to Sept . 2006 at the Università degli Studi di Milano Department of Computer Science

  2006cites this paper
• Shape Analysis by Predicate Abstraction

  2005cites this paper
• Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists

  2005cites this paper
• Automated Compositional Abstraction Re nement for Concurrent C Programs : A Two-Level Approach 1

  2005cites this paper
• Field Constraint Analysis

  2005cites this paper
• Abstraction of Graph Transformation Systems by Temporal Logic and Its Verification

  2005cites this paper
• Boolean Heaps

  2005cites this paper
• Computer Science and Artificial Intelligence Laboratory On Field Constraint Analysis

  2005cites this paper
• Symbolic Shape Analysis Diploma Thesis

  2004cites this paper
• Efficient Verification of Sequential and Concurrent C Programs

  2004cites this paper
• Modular verification of software components in C

  2004cites this paper
• Boolean Algebra of Shape Analysis Constraints

  2004cites this paper
• Ecien t Verication of Sequential and Concurrent C

  2004cites this paper
• Modular verification of software components in C

  2003cites this paper
• Predicate Abstraction with Minimum Predicates

  2003cites this paper
• Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach

  2003cites this paper
• pagesAutomated Compositional Abstra tionRe nement for Con urrent C Programs : A Two-Level Approa h 1

  2003cites this paper
• Comparing Abstraction Refinement Algorithms

  2003cites this paper
• General-Purpose Assertions for Data Structures

  year unknowncites this paper