Tasks in modular proofs of concurrent algorithms

DOI10.1007/978-3-030-34992-9_6zbMath1543.68197MaRDI QIDQ6536328

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

Publication date: 19 April 2024

zbMATH Keywords

verificationformal methodsconcurrent algorithmsrenaming

Mathematics Subject Classification ID

Parallel algorithms in computer science (68W10) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Distributed algorithms (68W15) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Unnamed Item
• The renaming problem in shared memory systems: an introduction
• Tight bounds for adopt-commit objects
• A scalable lock-free stack algorithm
• More \(choices\) allow more \(faults\): Set consensus problems in totally asynchronous systems
• Elimination trees and the construction of pools and stacks
• Modular verification of concurrency-aware linearizability
• Wait-free algorithms for fast, long-lived renaming
• Round-by-round fault detectors (extended abstract)
• Byzantizing Paxos by Refinement
• Concurrent Programming: Algorithms, Principles, and Foundations
• Renaming in an asynchronous environment
• Unifying Concurrent Objects and Distributed Tasks
• The BG distributed simulation algorithm
• Verifying linearizability with hindsight
• Generalized FLP impossibility result for t-resilient asynchronous computations
• Nonblocking Concurrent Data Structures with Condition Synchronization
• MCMT: A Model Checker Modulo Theories
• Proving a non-blocking algorithm for process renaming with TLA\textsuperscript{+}

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