Synchronizing the asynchronous

DOI10.4230/LIPICS.CONCUR.2018.21MaRDI QIDQ5009435zbMATH OpenFDO

Authors Bernhard Kragl, Shaz Qadeer, Thomas A. Henzinger

Publication date 4 August 2021

Full work available at URL https://doi.org/10.4230/LIPICS.CONCUR.2018.21

zbMATH Keywords

synchronizationcommutativityrefinementdeductive verificationconcurrent programsasynchronous programsatomic actionLipton redmover types

Mathematics Subject Classification ID

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

Recommendations

• Interprocedural analysis of asynchronous programs
• scientific article; zbMATH DE number 6774232
• Verifiable design of asynchronous software
• Synthesis of asynchronous reactive programs from temporal specifications
• scientific article; zbMATH DE number 1361122

Cites work

• scientific article; zbMATH DE number 6774232 (Why is no real title available?)
• A calculus of atomic actions
• Dafny: an automatic program verifier for functional correctness
• Reduction
• Refinement for structured concurrent programs
• Resources, concurrency, and local reasoning
• Transactions for software model checking
• Verifying robustness of event-driven asynchronous programs against concurrency
• \textsc{PSync}: a partially synchronous language for fault-tolerant distributed algorithms

Cited in

(23)

• Verifying the correctness of distributed systems via mergeable parallelism
• Specifying stateful asynchronous properties for distributed programs
• Ghost signals: verifying termination of busy waiting
• Inferring Synchronization under Limited Observability
• Abstraction-guided synthesis of synchronization
• Guessing the buffer bound for k-synchronizability
• On the k-synchronizability of systems
• Synchronization
• Synchronizing Moore and Spiegel
• A reduction theorem for randomized distributed algorithms under weak adversaries
• Eliminating message counters in synchronous threshold automata
• Analysis of asynchronous programs with event-based synchronization
• Automated synthesis of asynchronizations
• Asynchronous exclusive selection
• Verifying robustness of event-driven asynchronous programs against concurrency
• Verifiable design of asynchronous software
• Guessing the Buffer Bound for k-Synchronizability
• Verifying asynchronous event-driven programs using partial abstract transformers
• Asynchronous Cooperative Contracts for Cooperative Scheduling
• Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
• A reduction semantics for direct-style asynchronous observables
• Interprocedural analysis of asynchronous programs
• Synchronizing the consistency relation

Describes a project that uses

Uses Software

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

This page was built for publication: Synchronizing the asynchronous

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