Compositional shape analysis by means of bi-abduction

DOI10.1145/1480881.1480917MaRDI QIDQ5261525zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(35)

• Invariants synthesis over a combined domain for automated program verification
• Make flows small again: revisiting the flow framework
• Separation logics and modalities: a survey
• Scalable algorithms for abduction via enumerative syntax-guided synthesis
• Practical Tactics for 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
• From invariant checking to invariant inference using randomized search
• Parameterized synthesis for fragments of first-order logic over data words
• Ideal abstractions for well-structured transition systems
• Forest automata for verification of heap manipulation
• Automatic inference of access permissions
• Bottom-Up Shape Analysis
• Symbolic execution proofs for higher order store programs
• Refinement to Imperative/HOL
• Efficient modular SMT-based model checking of pointer programs
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• A divide-and-conquer approach for analysing overlaid data structures
• Temporal property verification as a program analysis task
• A shape graph logic and a shape system
• Highly automated formal proofs over memory usage of assembly code
• Compositional shape analysis by means of bi-abduction
• Verifying pointer safety for programs with unknown calls
• Compositional may-must program analysis: unleashing the power of alternation
• Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis
• Region Analysis for Race Detection
• Automated cyclic entailment proofs in separation logic
• Combining model checking and data-flow analysis
• An efficient cyclic entailment procedure in a fragment of separation logic
• Caper
• Precondition inference from intermittent assertions and application to contracts on collections
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Interprocedural shape analysis for effectively cutpoint-free programs
• 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)