Iris

DOI10.1145/2676726.2676980zbMath1346.68135MaRDI 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

invariants; higher-order logic; compositional verification; separation logic; atomicity; fine-grained concurrency; partial commutative monoids

Mathematics Subject Classification ID

03B70: Logic in computer science

68Q60: Specification and verification (program logics, model checking, etc.)

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Related Items

Iris from the ground up: A modular foundation for higher-order concurrent separation logic, Unnamed Item, Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems, RustHorn: CHC-Based Verification for Rust Programs, Bringing Order to the Separation Logic Jungle, Steps in modular specifications for concurrent modules (invited tutorial paper), 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, Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits, 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, An adaptation-complete proof system for local reasoning about cloud storage systems, \( \pi\) with leftovers: a mechanisation in Agda, On models of higher-order separation logic, A game semantics of concurrent separation logic, Modular Termination Verification for Non-blocking Concurrency, Transfinite Step-Indexing: Decoupling Concrete and Logical Steps, Caper, The Essence of Higher-Order Concurrent Separation Logic, A Higher-Order Logic for Concurrent Termination-Preserving Refinement, Abstract Specifications for Concurrent Maps