Compositional Shape Analysis by Means of Bi-Abduction
From MaRDI portal
Publication:5395670
DOI10.1145/2049697.2049700zbMath1281.68155OpenAlexW1992012690WikidataQ59410746 ScholiaQ59410746MaRDI QIDQ5395670
Hongseok Yang, Dino Distefano, Cristiano Calcagno, Peter W. O'Hearn
Publication date: 17 February 2014
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://ora.ox.ac.uk/objects/uuid:bcfefe74-a79c-4155-8160-c51f92f05466
Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (32)
Program Verification with Separation Logic ⋮ A stone-type duality theorem for separation logic via its underlying bunched logics ⋮ Algebraic program analysis ⋮ Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) ⋮ Model Checking Concurrent Programs ⋮ Decision Procedure for Entailment of Symbolic Heaps with Arrays ⋮ Disproving Inductive Entailments in Separation Logic via Base Pair Approximation ⋮ Generalized arrays for Stainless frames ⋮ Undecidability of Propositional Separation Logic and Its Neighbours ⋮ Unnamed Item ⋮ A proof procedure for separation logic with inductive definitions and data ⋮ Proof tactics for assertions in separation logic ⋮ Using Unified Model Checking to Verify Heaps ⋮ Foundations for entailment checking in quantitative separation logic ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ Unnamed Item ⋮ A learning-based approach to synthesizing invariants for incomplete verification engines ⋮ Selective monitoring ⋮ Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation ⋮ Strong-separation logic ⋮ Automated repair of heap-manipulating programs using deductive synthesis ⋮ Compositional satisfiability solving in separation logic ⋮ Verify heaps via unified model checking ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On Temporal and Separation Logics ⋮ Unnamed Item ⋮ An adaptation-complete proof system for local reasoning about cloud storage systems ⋮ Invariants Synthesis over a Combined Domain for Automated Program Verification ⋮ Reasoning about block-based cloud storage systems via separation logic ⋮ A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
Uses Software
This page was built for publication: Compositional Shape Analysis by Means of Bi-Abduction
