Modular termination verification for non-blocking concurrency

DOI10.1007/978-3-662-49498-1_8MaRDI QIDQ2802477zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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)

Recommendations

• Modular verification of a non-blocking stack
• Compositional verification of termination-preserving refinement of concurrent programs
• Proving that non-blocking algorithms don't block
• Reasoning about nonblocking concurrency
• scientific article; zbMATH DE number 176727

Cites work

• scientific article; zbMATH DE number 2090840 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• Compositional verification of termination-preserving refinement of concurrent programs
• Impredicative concurrent abstract predicates
• Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
• Modular termination verification for non-blocking concurrency
• Proving that non-blocking algorithms don't block
• Quantitative reasoning for proving lock-freedom
• Separation logic and abstraction
• Steps in modular specifications for concurrent modules (invited tutorial paper)
• Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
• Views, compositional reasoning for concurrent programs

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 perspective on specifying and verifying concurrent modules
• Abstract specifications for concurrent maps
• A higher-order logic for concurrent termination-preserving refinement
• Modular termination verification for non-blocking concurrency

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)