Modular termination verification for non-blocking concurrency
DOI10.1007/978-3-662-49498-1_8zbMATH Open1335.68074OpenAlexW2344539696MaRDI QIDQ2802477FDOQ2802477
Authors: Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, Julian Sutherland 
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
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Views, compositional reasoning for concurrent programs
- Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
- Impredicative concurrent abstract predicates
- Proving that non-blocking algorithms don't block
- Separation logic and abstraction
- Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
- Quantitative reasoning for proving lock-freedom
- Modular termination verification for non-blocking concurrency
- Compositional verification of termination-preserving refinement of concurrent programs
- Steps in modular specifications for concurrent modules (invited tutorial paper)
Cited In (7)
- Modular verification of a non-blocking stack
- Ghost signals: verifying termination of busy waiting
- Concise outlines for a complex logic: a proof outline checker for TaDA
- A higher-order logic for concurrent termination-preserving refinement
- Modular termination verification for non-blocking concurrency
- A perspective on specifying and verifying concurrent modules
- Abstract specifications for concurrent maps
This page was built for publication: Modular termination verification for non-blocking concurrency
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2802477)
