The following pages link to Iris (Q2819854):
Displaying 21 items.
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (Q670699) (← links)
- A perspective on specifying and verifying concurrent modules (Q1648035) (← links)
- VST-Floyd: a separation logic tool to verify correctness of C programs (Q1663238) (← links)
- Lewis meets Brouwer: constructive strict implication (Q1688950) (← links)
- An adaptation-complete proof system for local reasoning about cloud storage systems (Q2072067) (← links)
- \( \pi\) with leftovers: a mechanisation in Agda (Q2117018) (← links)
- On models of higher-order separation logic (Q2130583) (← links)
- A game semantics of concurrent separation logic (Q2130597) (← links)
- Modular Termination Verification for Non-blocking Concurrency (Q2802477) (← links)
- Transfinite Step-Indexing: Decoupling Concrete and Logical Steps (Q2802498) (← links)
- Caper (Q2988651) (← links)
- The Essence of Higher-Order Concurrent Separation Logic (Q2988664) (← links)
- A Higher-Order Logic for Concurrent Termination-Preserving Refinement (Q2988673) (← links)
- Abstract Specifications for Concurrent Maps (Q2988678) (← links)
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic (Q4625160) (← links)
- Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems (Q5041100) (← links)
- RustHorn: CHC-Based Verification for Rust Programs (Q5041108) (← links)
- Bringing Order to the Separation Logic Jungle (Q5055998) (← links)
- (Q5090915) (← links)
- Steps in modular specifications for concurrent modules (invited tutorial paper) (Q5971389) (← links)
- Concise outlines for a complex logic: a proof outline checker for TaDA (Q6145023) (← links)
