Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification

DOI10.1007/978-3-540-87603-8_47zbMath1156.68352OpenAlexW1868552112MaRDI QIDQ3535380

Ken Pierce, Cliff B. Jones

Publication date: 11 November 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-87603-8_47

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (5)

Possible values: exploring a concept for concurrency ⋮ Inter-process buffers in separation logic with rely-guarantee ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ Explanation of two non-blocking shared-variable communication algorithms ⋮ Elucidating concurrent algorithms via layers of abstraction and reification

Cites Work

• Inter-process buffers in separation logic with rely-guarantee
• Splitting atoms safely
• Non-deterministic data types: Models and implementations
• Ramifications of metastability in bit variables explored via Simpson's 4-slot mechanism
• Modular Safety Checking for Fine-Grained Concurrency
• Tentative steps toward a development method for interfering programs
• The B-Book
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification