Pages that link to "Item:Q5261525"
From MaRDI portal
The following pages link to Compositional shape analysis by means of bi-abduction (Q5261525):
Displaying 31 items.
- Symbolic execution proofs for higher order store programs (Q287265) (← links)
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic (Q436400) (← links)
- From invariant checking to invariant inference using randomized search (Q518404) (← links)
- Verifying pointer safety for programs with unknown calls (Q604389) (← links)
- A shape graph logic and a shape system (Q744329) (← links)
- VST-Floyd: a separation logic tool to verify correctness of C programs (Q1663238) (← links)
- Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free (Q2058383) (← links)
- A relational shape abstract domain (Q2058389) (← links)
- Scalable algorithms for abduction via enumerative syntax-guided synthesis (Q2096443) (← links)
- Parameterized synthesis for fragments of first-order logic over data words (Q2200816) (← links)
- A divide-and-conquer approach for analysing overlaid data structures (Q2441710) (← links)
- Temporal property verification as a program analysis task (Q2441713) (← links)
- Forest automata for verification of heap manipulation (Q2441715) (← links)
- Invariants Synthesis over a Combined Domain for Automated Program Verification (Q2842643) (← links)
- Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data (Q2891398) (← links)
- Automatic Inference of Access Permissions (Q2891412) (← links)
- Ideal Abstractions for Well-Structured Transition Systems (Q2891435) (← links)
- Refinement to Imperative/HOL (Q2945637) (← links)
- Caper (Q2988651) (← links)
- Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic (Q2988661) (← links)
- Precondition Inference from Intermittent Assertions and Application to Contracts on Collections (Q3075478) (← links)
- Combining Model Checking and Data-Flow Analysis (Q3176374) (← links)
- Practical Tactics for Separation Logic (Q3183539) (← links)
- Region Analysis for Race Detection (Q3392925) (← links)
- Bottom-Up Shape Analysis (Q3392926) (← links)
- Separation logics and modalities: a survey (Q4586138) (← links)
- Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs (Q4916088) (← links)
- Highly Automated Formal Proofs over Memory Usage of Assembly Code (Q5164171) (← links)
- Automated Cyclic Entailment Proofs in Separation Logic (Q5200020) (← links)
- Make flows small again: revisiting the flow framework (Q6535380) (← links)
- Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis (Q6536280) (← links)
