Pages that link to "Item:Q3612005"
From MaRDI portal
The following pages link to Modular Safety Checking for Fine-Grained Concurrency (Q3612005):
Displayed 19 items.
- Explanation of two non-blocking shared-variable communication algorithms (Q469352) (← links)
- Proving linearizability with temporal logic (Q539223) (← links)
- Elucidating concurrent algorithms via layers of abstraction and reification (Q539423) (← links)
- Inter-process buffers in separation logic with rely-guarantee (Q613139) (← links)
- Balancing expressiveness in formal approaches to concurrency (Q890478) (← links)
- Mechanized proofs of opacity: a comparison of two techniques (Q1673658) (← 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)
- On the relation between concurrent separation logic and concurrent Kleene algebra (Q2347904) (← links)
- Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example (Q2418046) (← links)
- A Program Construction and Verification Tool for Separation Logic (Q2941173) (← links)
- A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures (Q2946743) (← links)
- Caper (Q2988651) (← links)
- Automated Theorem Proving for Assertions in Separation Logic with All Connectives (Q3454118) (← links)
- Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification (Q3535380) (← links)
- Model Checking Simulation Rules for Linearizability (Q4571132) (← links)
- Verifying Opacity of a Transactional Mutex Lock (Q5206950) (← links)
- Reasoning about Separation Using Abstraction and Reification (Q5268439) (← links)
- Concurrent Separation Logic and Operational Semantics (Q5739365) (← links)
- Concise outlines for a complex logic: a proof outline checker for TaDA (Q6145023) (← links)