Reasoning about Optimistic Concurrency Using a Program Logic for History

DOI10.1007/978-3-642-15375-4_27zbMath1287.03071OpenAlexW1824790454MaRDI QIDQ3584944

Zhong Shao, Ming Fu, Yu Zhang, Xinyu Feng, Yong Li

Publication date: 31 August 2010

Published in: CONCUR 2010 - Concurrency Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-15375-4_27

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic in computer science (03B70) 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 (5)

A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ A relational shape abstract domain ⋮ Formal Verification of a Lock-Free Stack with Hazard Pointers ⋮ On the relation between concurrent separation logic and concurrent Kleene algebra

This page was built for publication: Reasoning about Optimistic Concurrency Using a Program Logic for History