Compositional shape analysis by means of bi-abduction
From MaRDI portal
Publication:5261525
Recommendations
Cited in
(35)- Highly automated formal proofs over memory usage of assembly code
- Unified reasoning about robustness properties of symbolic-heap separation logic
- Bottom-Up Shape Analysis
- Ideal abstractions for well-structured transition systems
- Interprocedural shape analysis for effectively cutpoint-free programs
- 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
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Make flows small again: revisiting the flow framework
- Temporal property verification as a program analysis task
- Verifying pointer safety for programs with unknown calls
- Efficient modular SMT-based model checking of pointer programs
- 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
- Practical Tactics for Separation Logic
- An efficient cyclic entailment procedure in a fragment of 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
- VST-Floyd: a separation logic tool to verify correctness of C programs
- Invariants synthesis over a combined domain for automated program verification
- Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis
- Caper
- Parameterized synthesis for fragments of first-order logic over data words
- Scalable algorithms for abduction via enumerative syntax-guided synthesis
- Compositional shape analysis by means of bi-abduction
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)
