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

asynchronous programsatomic actioncommutativityconcurrent programsdeductive verificationLipton redmover typesrefinementsynchronization

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

• \textsc{PSync}: a partially synchronous language for fault-tolerant distributed algorithms
• A calculus of atomic actions
• Dafny: an automatic program verifier for functional correctness
• scientific article; zbMATH DE number 6774232 (Why is no real title available?)
• 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

Cited in

(24)

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

Describes a project that uses

Uses Software

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

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)