The Essence of Higher-Order Concurrent Separation Logic

DOI10.1007/978-3-662-54434-1_26zbMath1485.68069OpenAlexW2596377803MaRDI QIDQ2988664

Robbert Krebbers, Aleš Bizjak, Jacques-Henri Jourdan, Ralf Jung, Derek R. Dreyer, Lars Birkedal

Publication date: 19 May 2017

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-54434-1_26

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) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems, On models of higher-order separation logic, A game semantics of concurrent separation logic, VST-Floyd: a separation logic tool to verify correctness of C programs, Proof tactics for assertions in separation logic, Parameterized synthesis for fragments of first-order logic over data words, Iris from the ground up: A modular foundation for higher-order concurrent separation logic, Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits, Highly Automated Formal Proofs over Memory Usage of Assembly Code, Linear capabilities for fully abstract compilation of separation-logic-verified code

Uses Software

• Coq
• Toolchain

Cites Work

• Unnamed Item
• Resources, concurrency, and local reasoning
• Proving assertions about parallel programs
• Monads on symmetric monoidal closed categories
• Strong functors and monoidal monads
• Iris
• Higher-order ghost state
• A very modal model of a modern, major, general type system
• Deny-Guarantee Reasoning
• Guarded commands, nondeterminacy and formal derivation of programs
• The Logic of Bunched Implications
• BI as an assertion language for mutable data structures
• Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
• A relational modal logic for higher-order stateful ADTs
• Permission accounting in separation logic
• Modular Reasoning about Separation of Concurrent Data Structures
• Interactive proofs in higher-order concurrent separation logic
• A relational model of types-and-effects in higher-order concurrent separation logic
• Expressive modular fine-grained concurrency specification
• Verified Compilation for Shared-Memory C
• Impredicative Concurrent Abstract Predicates
• Oracle Semantics for Concurrent Separation Logic
• Program Logics for Certified Compilers