Towards a Thread-Local Proof Technique for Starvation Freedom

DOI10.1007/978-3-319-33693-0_13zbMath1354.68179OpenAlexW2475115935MaRDI QIDQ2814127

Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim

Publication date: 17 June 2016

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

Full work available at URL: https://doi.org/10.1007/978-3-319-33693-0_13

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Uses Software

• RGITL

Cites Work

• Unnamed Item
• Myths about the mutual exclusion problem
• An axiomatic proof technique for parallel programs
• Model checking and abstraction to the aid of parameterized systems (a survey)
• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• A program logic for concurrent objects under fair scheduling
• Compositional Termination Proofs for Multi-threaded Programs
• A Marriage of Rely/Guarantee and Separation Logic
• Temporal Verification of Reactive Systems: Response
• A new solution of Dijkstra's concurrent programming problem
• Proving that non-blocking algorithms don't block

This page was built for publication: Towards a Thread-Local Proof Technique for Starvation Freedom