Compositional shape analysis by means of bi-abduction

No abstract is available for this paper.

• Publication year

  2009

• Venue

  ACM-SIGACT Symposium on Principles of Programming Languages

• Publication date

  2009-01-21

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/1480881.1480917
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• BI as an assertion language for mutable data structures

  2011influential reference
• Memory Leaks Detection in Java by Bi-abductive Inference

  2010cited by this paper
• Verifying pointer safety for programs with unknown calls

  2010cited by this paper
• Software model checking

  2009cited by this paper
• Bi-abductive Resource Invariant Synthesis

  2009cited by this paper
• Separation and information hiding

  2009cited by this paper
• Bottom-Up Shape Analysis

  2009cited by this paper
• Relational inductive shape analysis

  2008cited by this paper
• Heap Assumptions on Demand

  2008cited by this paper
• Efficient Context-Sensitive Shape Analysis with Graph Based Heap Models

  2008cited by this paper
• Monotonic Abstraction for Programs with Dynamic Memory Heaps

  2008cited by this paper
• Sufficient Preconditions for Modular Assertion Checking

  2008cited by this paper
• Lifting abstract interpreters to quantified logical domains

  2008cited by this paper
• Scalable Shape Analysis for Systems Code

  2008cited by this paper
• Enhancing Program Verification with Lemmas

  2008cited by this paper
• jStar: towards practical verification for java

  2008cited by this paper
• Practical memory leak detector based on parameterized procedural summaries

  2008cited by this paper
• Footprint Analysis: A Shape Analysis That Discovers Preconditions

  2007cited by this paper
• Backward Analysis for Inferring Quantified Preconditions Technical Report TR-2007-1201

  2007cited by this paper
• Local Action and Abstract Separation Logic

  2007cited by this paper
• Thread-modular shape analysis

  2007cited by this paper
• Shape Analysis by Graph Decomposition

  2007cited by this paper
• Arithmetic Strengthening for Shape Analysis

  2007cited by this paper
• Low-Level Library Analysis and Summarization

  2007cited by this paper
• Shape Analysis with Structural Invariant Checkers

  2007cited by this paper
• Automated Verification of Shape and Size Properties Via Separation Logic

  2007cited by this paper
• Computing Procedure Summaries for Interprocedural Analysis

  2007cited by this paper
• Shape analysis with inductive recursion synthesis

  2007cited by this paper
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures

  2006cited by this paper
• Thorough static analysis of device drivers

  2006cited by this paper
• Interprocedural Shape Analysis with Separated Heap Abstractions

  2006cited by this paper
• Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic

  2006cited by this paper
• A Local Shape Analysis Based on Separation Logic

  2006cited by this paper
• Abstraction for Shape Analysis with Fast and Precise Transformers

  2006cited by this paper
• A Complete Classification of the Complexity of Propositional Abduction

  2006cited by this paper
• Shape Analysis by Predicate Abstraction

  2005cited by this paper
• Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking

  2005cited by this paper
• Boolean Heaps

  2005cited by this paper
• Region-based shape analysis with tracked locations

  2005cited by this paper
• Lightweight object specification with typestates

  2005cited by this paper
• Symbolic Execution with Separation Logic

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

  2005cited by this paper
• Smallfoot: Modular Automatic Assertion Checking with Separation Logic

  2005cited by this paper
• The ASTREÉ Analyzer

  2005cited by this paper
• Interprocedural Shape Analysis for Cutpoint-Free Programs

  2005cited by this paper
• A semantics for procedure local heaps and its abstractions

  2005cited by this paper
• The ASTR ´ EE Analyzer

  2005cited by this paper
• A Decidable Fragment of Separation Logic

  2004cited by this paper
• Separation and information hiding

  2004cited by this paper
• Typestates for Objects

  2004cited by this paper
• Resources, Concurrency and Local Reasoning

  2004cited by this paper
• Possible worlds and resources: the semantics of BI

  2004cited by this paper
• Bottom-Up and Top-Down Context-Sensitive Summary-Based Pointer Analysis

  2004cited by this paper
• CSSV: towards a realistic tool for statically detecting all buffer overflows in C

  2003cited by this paper
• On computing all abductive explanations

  2002cited by this paper
• Lazy abstraction

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

  2002cited by this paper
• Separation logic: a logic for shared mutable data structures

  2002cited by this paper
• Role analysis

  2002cited by this paper
• Modular Static Program Analysis

  2002cited by this paper
• Local Reasoning for Stateful Programs

  2001cited by this paper
• Local Reasoning about Programs that Alter Data Structures

  2001cited by this paper
• Calculating sharp adaptation rules

  2001cited by this paper
• Compositional separate modular static analysis of programs by abstract interpretation

  2001cited by this paper
• Hoare Logic and Auxiliary Variables

  1999cited by this paper
• Compositional pointer and escape analysis for Java programs

  1999cited by this paper
• Solving shape-analysis problems in languages with destructive updating

  1996cited by this paper
• Is it a tree, a DAG, or a cyclic graph? A shape analysis for heap-directed pointers in C

  1996cited by this paper
• Precise interprocedural dataflow analysis via graph reachability

  1995cited by this paper
• Abductive Analysis of Modular Logic Programs

  1994cited by this paper
• Parallel Abduction in Logic Programming

  1994cited by this paper
• Approaches to abductive reasoning: an overview

  1993cited by this paper
• The complexity of logic-based abduction

  1993cited by this paper
• Program Flow Analysis: Theory and Application

  1981cited by this paper
• Soundness and Completeness of an Axiom System for Program Verification

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

  1977cited by this paper
• Procedures and parameters: An axiomatic approach

  1971cited by this paper
• Collected Papers of Charles Sanders Peirce

  1936cited by this paper
• Collected Papers of Charles Sanders Peirce

  1935cited by this paper
• To appear in: CAV 2007. Shape Analysis for Composite Data Structures

  year unknowncited by this paper

• SemTaint: A scalable taint analysis approach for JavaWeb frameworks and composite containers

  2026cites this paper
• LLMs versus the Halting Problem: Revisiting Program Termination Prediction

  2026cites this paper
• Vul2image: A Quick Image-inspired and CNN-based Vulnerability Detection system

  2026cites this paper
• Same Engine, Multiple Gears: Parallelizing Fixpoint Iteration at Different Granularities (Extended Version)

  2026cites this paper
• QCP: A Practical Separation Logic-based C Program Verification Tool

  2025cites this paper
• LAMeD: LLM-generated Annotations for Memory Leak Detection

  2025cites this paper
• Compositional Symbolic Execution for the Next 700 Memory Models

  2025cites this paper
• Non-Termination Proving: 100 Million LoC and Beyond

  2025influential citation
• H-Houdini: Scalable Invariant Learning

  2025cites this paper
• Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis (Artifact)

  2025cites this paper
• Improvements in Software Verification and Witness Validation: SV-COMP 2025

  2025cites this paper
• BugScope: Learn to Find Bugs Like Human

  2025cites this paper
• Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic

  2025cites this paper
• Verifying Tree-Manipulating Programs via CHCs

  2025cites this paper
• Program Skeletons for Automated Program Translation

  2025cites this paper
• RepoAudit: An Autonomous LLM-Agent for Repository-Level Code Auditing

  2025cites this paper
• Counterexample-Guided Inference of Modular Specifications

  2025cites this paper
• Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification

  2025cites this paper
• Compositional Verification in Concurrent Separation Logic with Permissions Regions

  2025cites this paper
• FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs

  2025cites this paper
• Enhancing Compositional Static Analysis with Dynamic Analysis

  2024influential citation
• Automatic Policy Synthesis and Enforcement for Protecting Untrusted Deserialization

  2024cites this paper
• Verifying the Option Type with Rely–Guarantee Reasoning

  2024cites this paper
• Deciding Boolean Separation Logic via Small Models (Technical Report)

  2024cites this paper
• Precise Compositional Buffer Overflow Detection via Heap Disjointness

  2024cites this paper
• Generically Automating Separation Logic by Functors, Homomorphisms, and Modules

  2024cites this paper
• Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification

  2024cites this paper
• A Mixed Methods Study on the Implications of Unsafe Rust for Interoperation, Encapsulation, and Tooling

  2024cites this paper
• Sound Borrow-Checking for Rust via Symbolic Semantics

  2024cites this paper
• Enhancing Field Tracking and Interprocedural Analysis to Find More Null Pointer Exceptions

  2024cites this paper
• Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects

  2024cites this paper
• Inference of Robust Reachability Constraints

  2024influential citation
• Specification and Verification for Unrestricted Algebraic Effects and Handling

  2024cites this paper
• How About Bug-Triggering Paths? - Understanding and Characterizing Learning-Based Vulnerability Detectors

  2024cites this paper
• Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses

  2024cites this paper
• Towards Integration of Syntactic and Semantic Vulnerability Patterns

  2024cites this paper
• LLMDFA: Analyzing Dataflow in Code with Large Language Models

  2024cites this paper
• When Dataflow Analysis Meets Large Language Models

  2024cites this paper
• Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis

  2024cites this paper
• Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations

  2024cites this paper
• State of the Art in Software Verification and Witness Validation: SV-COMP 2024

  2024cites this paper
• Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq

  2024influential citation
• Representation of Peano Arithmetic in Separation Logic

  2024cites this paper
• Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version)

  2024cites this paper
• Everything is Good for Something: Counterexample-Guided Directed Fuzzing via Likely Invariant Inference

  2024cites this paper
• AXA: Cross-Language Analysis through Integration of Single-Language Analyses

  2024cites this paper
• A Proof Procedure for Separation Logic with Inductive Definitions and Data

  2023cites this paper
• Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning

  2023cites this paper
• Make flows small again: revisiting the flow framework

  2023cites this paper
• Revealing Sources of (Memory) Errors via Backward Analysis

  2023cites this paper
• A Product of Shape and Sequence Abstractions

  2023cites this paper
• On the Relationship between Code Verifiability and Understandability

  2023cites this paper
• Staged Specification Logic for Verifying Higher-Order Imperative Programs

  2023cites this paper
• Affine Disjunctive Invariant Generation with Farkas' Lemma

  2023cites this paper
• Context-Aware Separation Logic

  2023cites this paper
• Expressiveness Results for an Inductive Logic of Separated Relations

  2023cites this paper
• Generalized Program Sketching by Abstract Interpretation and Logical Abduction

  2023cites this paper
• Hybrid Inlining: A Framework for Compositional and Context-Sensitive Static Analysis

  2023cites this paper
• Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects

  2023influential citation
• Automated Synthesis of Software Contracts with KindSpec

  2023cites this paper
• An Interactive SMT Tactic in Coq using Abductive Reasoning

  2023cites this paper
• Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration

  2023influential citation
• Learning to Boost Disjunctive Static Bug-Finders

  2023cites this paper
• Monoidal Hoare Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning

  2022cites this paper
• Foundations for Entailment Checking in Quantitative Separation Logic (extended version)

  2022cites this paper
• Anchor: Fast and Precise Value-flow Analysis for Containers via Memory Orientation

  2022cites this paper
• Hybrid Inlining: A Compositional and Context Sensitive Static Analysis Framework

  2022cites this paper
• Efficient Modular SMT-Based Model Checking of Pointer Programs

  2022cites this paper
• Infrared: A Meta Bug Detector

  2022cites this paper
• S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs

  2022cites this paper
• Diaframe: automated verification of fine-grained concurrent programs in Iris

  2022influential citation
• Interactive Abstract Interpretation: Reanalyzing Whole Programs for Cheap

  2022cites this paper
• An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic

  2022cites this paper
• Towards Concurrent Quantitative Separation Logic

  2022cites this paper
• Finding real bugs in big programs with incorrectness logic

  2022influential citation
• STATIC FILE PATH ANALYSIS FOR RELIABLE RESOURCE LOCATING

  2022cites this paper
• Automated Program Analysis: Revisiting Precondition Inference through Constraint Acquisition

  2022cites this paper
• A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning

  2022cites this paper
• Designing a Provenance Analysis for SGX Enclaves

  2022cites this paper
• Gradual C0: Symbolic Execution for Gradual Verification

  2022cites this paper
• Precise Divide-By-Zero Detection with Affirmative Evidence

  2022influential citation
• The Static Analyzer Infer in SV-COMP (Competition Contribution)

  2022cites this paper
• InfERL: scalable and extensible Erlang static analysis

  2022cites this paper
• Low-Level Bi-Abduction

  2022influential citation
• Exposing Vulnerable Paths: Enhance Static Analysis with Lightweight Symbolic Execution

  2021cites this paper
• The First Fifteen Years of the Verified Software Project

  2021influential citation
• On the Real-World Effectiveness of Static Bug Detectors at Finding Null Pointer Exceptions

  2021cites this paper
• Reasoning about Reconfigurations of Distributed Systems

  2021cites this paper
• Solver-Aided Constant-Time Hardware Verification

  2021cites this paper
• Software engineering techniques for statically analyzing mobile apps: research trends, characteristics, and potential for industrial adoption

  2021cites this paper
• Hippodrome: Data Race Repair Using Static Analysis Summaries

  2021cites this paper
• Algebraic Program Analysis

  2021cites this paper
• Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper)

  2021cites this paper
• Understanding Execution Environment of File-Manipulation Scripts by Extracting Pre-Conditions

  2021cites this paper
• Compositional Vulnerability Detection with Insecurity Separation Logic

  2021influential citation
• Grammar-agnostic symbolic execution by token symbolization

  2021cites this paper
• Incremental Vulnerability Detection with Insecurity Separation Logic

  2021cites this paper
• Incremental Vulnerability Detection via Back-Propagating Symbolic Execution of Insecurity Separation Logic

  2021influential citation
• Specification synthesis with constrained Horn clauses

  2021cites this paper
• DeepWukong

  2021cites this paper