Tasks in modular proofs of concurrent algorithms

DOI10.1007/978-3-030-34992-9_6MaRDI QIDQ6536328zbMATH OpenFDO

Authors Armando Castañeda, Aurélie Hurault, Philippe Quéinnec, Matthieu Roy

Publication date 19 April 2024

Full work available at URL https://doi.org/10.1007/978-3-030-34992-9_6

zbMATH Keywords

concurrent algorithmsformal methodsrenamingverification

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) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Parallel algorithms in computer science (68W10) Distributed algorithms (68W15)

Recommendations

• Tasks in modular proofs of concurrent algorithms
• Proving a non-blocking algorithm for process renaming with TLA\textsuperscript{+}
• Specifying concurrent problems: beyond linearizability and up to tasks (extended abstract)
• Modular verification of a non-blocking stack
• Model-checking of correctness conditions for concurrent objects

Cites work

• A scalable lock-free stack algorithm
• A simplicial complex model for dynamic epistemic logic to study distributed task computability
• Byzantizing Paxos by refinement
• Concurrent programming: algorithms, principles, and foundations.
• Elimination trees and the construction of pools and stacks
• Generalized FLP impossibility result for t-resilient asynchronous computations
• MCMT: a model checker modulo theories
• Modular verification of concurrency-aware linearizability
• More \(choices\) allow more \(faults\): Set consensus problems in totally asynchronous systems
• Nonblocking Concurrent Data Structures with Condition Synchronization
• Proving a non-blocking algorithm for process renaming with TLA\textsuperscript{+}
• Renaming in an asynchronous environment
• Round-by-round fault detectors (extended abstract), unifying synchrony and asynchrony
• The BG distributed simulation algorithm
• The renaming problem in shared memory systems: an introduction
• The renaming problem: recent developments and open questions
• Tight bounds for adopt-commit objects
• Unifying Concurrent Objects and Distributed Tasks
• Verifying linearizability with hindsight
• Wait-free algorithms for fast, long-lived renaming

Cited in

(2)

• Tasks in modular proofs of concurrent algorithms
• Proving a non-blocking algorithm for process renaming with TLA\textsuperscript{+}

This page was built for publication: Tasks in modular proofs of concurrent algorithms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6536328)