Compositional shape analysis by means of bi-abduction

DOI10.1145/1480881.1480917zbMATH Open1315.68085OpenAlexW2154985136MaRDI QIDQ5261525FDOQ5261525

Authors: Cristiano Calcagno, Dino Distefano, 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

Recommendations

• Compositional shape analysis by means of bi-abduction
• Bottom-Up Shape Analysis
• scientific article; zbMATH DE number 1953039
• Tools and Algorithms for the Construction and Analysis of Systems
• Interprocedural Shape Analysis with Separated Heap Abstractions

zbMATH Keywords

proof theoryabductionprogram analysis

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Cited In (33)

• Bottom-Up Shape Analysis
• Combining Model Checking and Data-Flow Analysis
• Automatic Inference of Access Permissions
• Invariants Synthesis over a Combined Domain for Automated Program Verification
• Separation logics and modalities: a survey
• Region Analysis for Race Detection
• From invariant checking to invariant inference using randomized search
• Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
• Symbolic execution proofs for higher order store programs
• Make flows small again: revisiting the flow framework
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Temporal property verification as a program analysis task
• Ideal Abstractions for Well-Structured Transition Systems
• Efficient modular SMT-based model checking of pointer programs
• Verifying pointer safety for programs with unknown calls
• A divide-and-conquer approach for analysing overlaid data structures
• A shape graph logic and a shape system
• Refinement to Imperative/HOL
• Highly Automated Formal Proofs over Memory Usage of Assembly Code
• Automated cyclic entailment proofs in separation logic
• A relational shape abstract domain
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
• Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs
• An efficient cyclic entailment procedure in a fragment of separation logic
• Practical Tactics for Separation Logic
• Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data
• Precondition inference from intermittent assertions and application to contracts on collections
• Forest automata for verification of heap manipulation
• Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Caper
• Parameterized synthesis for fragments of first-order logic over data words
• Scalable algorithms for abduction via enumerative syntax-guided synthesis

This page was built for publication: Compositional shape analysis by means of bi-abduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5261525)