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 (35)

• Bottom-Up Shape Analysis
• Interprocedural shape analysis for effectively cutpoint-free programs
• Ideal abstractions for well-structured transition systems
• Separation logics and modalities: a survey
• Region Analysis for Race Detection
• From invariant checking to invariant inference using randomized search
• 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
• 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
• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• Refinement to Imperative/HOL
• Compositional may-must program analysis: unleashing the power of alternation
• 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
• An efficient cyclic entailment procedure in a fragment of separation logic
• Practical Tactics for Separation Logic
• Combining model checking and data-flow analysis
• Precondition inference from intermittent assertions and application to contracts on collections
• Forest automata for verification of heap manipulation
• Automatic inference of access permissions
• Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Invariants synthesis over a combined domain for automated program verification
• Caper
• Parameterized synthesis for fragments of first-order logic over data words
• Compositional shape analysis by means of bi-abduction
• Scalable algorithms for abduction via enumerative syntax-guided synthesis
• Highly automated formal proofs over memory usage of assembly code
• Unified reasoning about robustness properties of symbolic-heap separation logic

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)