Quantitative Reasoning for Proving Lock-Freedom

DOI10.1109/LICS.2013.18zbMath1366.68171MaRDI QIDQ5271049

Michael Marmar, Jan Hoffmann, Zhong Shao

Publication date: 3 July 2017

Published in: 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

zbMATH Keywords

concurrencyquantitative analysislock-freedomnon-blocking data structuresliveness, separation logic

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) Data structures (68P05)

Related Items (4)

A Higher-Order Logic for Concurrent Termination-Preserving Refinement ⋮ Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits ⋮ Modular Termination Verification for Non-blocking Concurrency ⋮ Two decades of automatic amortized resource analysis

This page was built for publication: Quantitative Reasoning for Proving Lock-Freedom