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

abductionprogram analysisproof theory

Mathematics Subject Classification ID

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

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

(37)

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

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)