Modular Termination Verification for Non-blocking Concurrency
From MaRDI portal
Publication:2802477
DOI10.1007/978-3-662-49498-1_8zbMath1335.68074OpenAlexW2344539696MaRDI QIDQ2802477
Thomas Dinsdale-Young, Julian Sutherland, Pedro da Rocha Pinto, Philippa Gardner
Publication date: 26 April 2016
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/10044/1/31740
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (6)
Ghost signals: verifying termination of busy waiting ⋮ A perspective on specifying and verifying concurrent modules ⋮ Concise outlines for a complex logic: a proof outline checker for TaDA ⋮ A Higher-Order Logic for Concurrent Termination-Preserving Refinement ⋮ Abstract Specifications for Concurrent Maps ⋮ Modular Termination Verification for Non-blocking Concurrency
Cites Work
- Unnamed Item
- Unnamed Item
- Modular Termination Verification for Non-blocking Concurrency
- Iris
- Views
- Compositional verification of termination-preserving refinement of concurrent programs
- Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
- Proving that non-blocking algorithms don't block
- Quantitative Reasoning for Proving Lock-Freedom
- Separation logic and abstraction
- Impredicative Concurrent Abstract Predicates
- Steps in modular specifications for concurrent modules (invited tutorial paper)
This page was built for publication: Modular Termination Verification for Non-blocking Concurrency
