Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos
DOI10.1007/s00236-013-0178-2zbMath1312.68153OpenAlexW2150869871MaRDI QIDQ2377304
Publication date: 28 June 2013
Published in: Acta Informatica (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00236-013-0178-2
[https%3A%2F%2Fportal.mardi4nfdi.de%2Fw%2Findex.php%3Ftitle%3D%2BSpecial%253ASearch%26search%3DNonnumerical+algorithms%26go%3DGo Nonnumerical algorithms (68W05)] [https%3A%2F%2Fportal.mardi4nfdi.de%2Fw%2Findex.php%3Ftitle%3D%2BSpecial%253ASearch%26search%3DSpecification+and+verification+%28program+logics%2C+model+checking%2C+etc.%29%26go%3DGo Specification and verification (program logics, model checking, etc.) (68Q60)] [https%3A%2F%2Fportal.mardi4nfdi.de%2Fw%2Findex.php%3Ftitle%3D%2BSpecial%253ASearch%26search%3DModels+and+methods+for+concurrent+and+distributed+computing+%28process+algebras%2C+bisimulation%2C+transition+nets%2C+etc.%29%26go%3DGo Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)]
Related Items (2)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Nonatomic dual bakery algorithm with bounded tokens
- The existence of refinement mappings
- Verification of sequential and concurrent programs
- Lock-free parallel and concurrent garbage collection by mark\&sweep
- A general lock-free algorithm using compare-and-swap
- A queue based mutual exclusion algorithm
- On interprocess communication. I: Basic formalism
- On interprocess communication. II: Algorithms
- Atomic semantics of nonatomic programs
- The verified incremental design of a distributed spanning tree algorithm: Extended abstract
- Proving assertions about parallel programs
- An axiomatic proof technique for parallel programs
- Bounded time-stamps
- A mechanically verified incremental garbage collector
- Distributed algorithms. 8th international workshop, WDAG 1994, Terschelling, The Netherlands, September 29 -- October 1, 1994. Proceedings
- A mechanical proof of Segall's PIF algorithm
- Using eternity variables to specify and prove a serializable database interface
- Lock-free dynamic hash tables with open addressing
- Nonatomic mutual exclusion with local spinning
- Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos
- Universal extensions to simulate specifications
- Efficient and practical constructions of LL/SC variables
- Bounded concurrent timestamp systems using vector clocks
- Temporal Verification of Reactive Systems: Response
- A New Approach to Proving the Correctness of Multiprocess Programs
- Self-stabilizing systems in spite of distributed control
- Proving the Correctness of Multiprocess Programs
- A new solution of Dijkstra's concurrent programming problem
- Wait-free linearization with a mechanical proof
- Shared-memory mutual exclusion: major research trends since 1986
- The Black-White Bakery Algorithm and Related Bounded-Space, Adaptive, Local-Spinning and FIFO Algorithms
- An axiomatic basis for computer programming
- The mutual exclusion problem
This page was built for publication: Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos
