Compositional shape analysis by means of bi-abduction
From MaRDI portal
Publication:5261525
DOI10.1145/1480881.1480917zbMath1315.68085OpenAlexW2154985136MaRDI QIDQ5261525
Dino Distefano, Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn
Publication date: 3 July 2015
Published in: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://ora.ox.ac.uk/objects/uuid:bcfefe74-a79c-4155-8160-c51f92f05466
Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (31)
Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data ⋮ Automatic Inference of Access Permissions ⋮ Ideal Abstractions for Well-Structured Transition Systems ⋮ Symbolic execution proofs for higher order store programs ⋮ Caper ⋮ Combining Model Checking and Data-Flow Analysis ⋮ Practical Tactics for Separation Logic ⋮ VST-Floyd: a separation logic tool to verify correctness of C programs ⋮ Verifying pointer safety for programs with unknown calls ⋮ Refinement to Imperative/HOL ⋮ Separation logics and modalities: a survey ⋮ An efficient cyclic entailment procedure in a fragment of separation logic ⋮ Efficient modular SMT-based model checking of pointer programs ⋮ Parameterized synthesis for fragments of first-order logic over data words ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ A divide-and-conquer approach for analysing overlaid data structures ⋮ Temporal property verification as a program analysis task ⋮ Forest automata for verification of heap manipulation ⋮ Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic ⋮ From invariant checking to invariant inference using randomized search ⋮ Highly Automated Formal Proofs over Memory Usage of Assembly Code ⋮ Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs ⋮ Automated Cyclic Entailment Proofs in Separation Logic ⋮ Precondition Inference from Intermittent Assertions and Application to Contracts on Collections ⋮ A shape graph logic and a shape system ⋮ Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free ⋮ A relational shape abstract domain ⋮ Region Analysis for Race Detection ⋮ Bottom-Up Shape Analysis ⋮ Invariants Synthesis over a Combined Domain for Automated Program Verification ⋮ Scalable algorithms for abduction via enumerative syntax-guided synthesis
This page was built for publication: Compositional shape analysis by means of bi-abduction
