Interactive proofs in higher-order concurrent separation logic

DOI10.1145/3009837.3009855zbMath1380.68341OpenAlexW2562833768WikidataQ130853219 ScholiaQ130853219MaRDI QIDQ5370856

Amin Timany, Robbert Krebbers, Lars Birkedal

Publication date: 20 October 2017

Published in: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://lirias.kuleuven.be/handle/123456789/553559

zbMATH Keywords

separation logiclogical relationsinteractive theorem provingCoqfine-grained concurrency

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 (12)

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems ⋮ On models of higher-order separation logic ⋮ Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms ⋮ VST-Floyd: a separation logic tool to verify correctness of C programs ⋮ Proof tactics for assertions in separation logic ⋮ Unnamed Item ⋮ 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 ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• Unnamed Item

This page was built for publication: Interactive proofs in higher-order concurrent separation logic