Ghost signals: verifying termination of busy waiting

DOI10.1007/978-3-030-81688-9_2zbMath1493.68097arXiv2010.11762OpenAlexW3185019351MaRDI QIDQ832247

Tobias Reinhard, Bart Jacobs

Publication date: 25 March 2022

Full work available at URL: https://arxiv.org/abs/2010.11762

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• ESC/Java
• VeriFast
• GitHub

Cites Work

• Unnamed Item
• The category-theoretic solution of recursive metric-space equations
• Deadlock-free monitors
• Modular Termination Verification for Non-blocking Concurrency
• A program logic for concurrent objects under fair scheduling
• Higher-order ghost state
• Deadlock-Free Channels and Locks
• A Basis for Verifying Multi-threaded Programs
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• An axiomatic basis for computer programming
• Concurrent Separation Logic and Operational Semantics
• A New Type System for Deadlock-Free Processes

This page was built for publication: Ghost signals: verifying termination of busy waiting