On the completeness of verifying message passing programs under bounded asynchrony

DOI10.1007/978-3-319-96142-2_23zbMath1511.68073arXiv1804.06612OpenAlexW2797596189MaRDI QIDQ6043166

Ahmed Bouajjani, Kailiang Ji, Shaz Qadeer, Constantin Enea

Publication date: 5 May 2023

Published in: Computer Aided Verification (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1804.06612

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) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (14)

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 ⋮ Multiparty half-duplex systems and synchronous communications ⋮ On the \(k\)-synchronizability of systems ⋮ Communicating finite-state machines, first-order logic, and star-free propositional dynamic logic ⋮ Unnamed Item ⋮ Fair refinement for asynchronous session types ⋮ Eliminating message counters in synchronous threshold automata ⋮ A reduction theorem for randomized distributed algorithms under weak adversaries ⋮ Unnamed Item ⋮ Non axiomatisability of positive relation algebras with constants, via graph homomorphisms ⋮ Input urgent semantics for asynchronous timed session types ⋮ Guessing the buffer bound for k-synchronizability

This page was built for publication: On the completeness of verifying message passing programs under bounded asynchrony