scientific article; zbMATH DE number 7378565

DOI10.4230/LIPIcs.CONCUR.2018.21MaRDI QIDQ5009435

Bernhard Kragl, Shaz Qadeer, Thomas A. Henzinger

Publication date: 4 August 2021

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

concurrent programssynchronizationrefinementcommutativitydeductive verificationasynchronous programsatomic actionLipton redmover types

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (8)

Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker ⋮ Verifying the correctness of distributed systems via mergeable parallelism ⋮ Guessing the Buffer Bound for k-Synchronizability ⋮ On the \(k\)-synchronizability of systems ⋮ Eliminating message counters in synchronous threshold automata ⋮ A reduction theorem for randomized distributed algorithms under weak adversaries ⋮ Unnamed Item ⋮ Guessing the buffer bound for k-synchronizability

Uses Software

• Dafny
• z3
• Ivy
• Verdi
• IronFleet
• Ivy

Cites Work

• Unnamed Item
• Unnamed Item
• Resources, concurrency, and local reasoning
• Refinement for structured concurrent programs
• PSync: a partially synchronous language for fault-tolerant distributed algorithms
• Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency
• Dafny: An Automatic Program Verifier for Functional Correctness
• Reduction
• A calculus of atomic actions

This page was built for publication: