Iris

DOI10.1145/2676726.2676980zbMath1346.68135OpenAlexW2147323041MaRDI QIDQ2819854

Derek R. Dreyer, Kasper Svendsen, Filip Sieczkowski, Aaron Joseph Turon, David Swasey, Ralf Jung, Lars Birkedal

Publication date: 29 September 2016

Published in: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2676726.2676980

zbMATH Keywords

invariantshigher-order logiccompositional verificationseparation logicatomicityfine-grained concurrencypartial commutative monoids

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (23)

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems ⋮ RustHorn: CHC-Based Verification for Rust Programs ⋮ On models of higher-order separation logic ⋮ A game semantics of concurrent separation logic ⋮ Caper ⋮ Bringing Order to the Separation Logic Jungle ⋮ A perspective on specifying and verifying concurrent modules ⋮ VST-Floyd: a separation logic tool to verify correctness of C programs ⋮ Lewis meets Brouwer: constructive strict implication ⋮ A formal logic for formal category theory ⋮ Concise outlines for a complex logic: a proof outline checker for TaDA ⋮ \textsf{LOGIC}: a Coq library for logics ⋮ Steps in modular specifications for concurrent modules (invited tutorial paper) ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ The Essence of Higher-Order Concurrent Separation Logic ⋮ A Higher-Order Logic for Concurrent Termination-Preserving Refinement ⋮ Abstract Specifications for Concurrent Maps ⋮ Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits ⋮ Unnamed Item ⋮ Modular Termination Verification for Non-blocking Concurrency ⋮ Transfinite Step-Indexing: Decoupling Concrete and Logical Steps ⋮ An adaptation-complete proof system for local reasoning about cloud storage systems ⋮ \( \pi\) with leftovers: a mechanisation in Agda

This page was built for publication: Iris