Model checking parameterized asynchronous shared-memory systems

DOI10.1007/s10703-016-0258-3zbMath1360.68584arXiv1505.06588OpenAlexW374648105MaRDI QIDQ5892422

Pierre Ganty, Javier Esparza, Antoine Durand-Gasselin, Rupak Majumdar

Publication date: 15 May 2017

Published in: Formal Methods in System Design, Computer Aided Verification (Search for Journal in Brave)

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

zbMATH Keywords

model checkingshared-memory systemsparametrized verification

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Liveness in broadcast networks, \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms, Reachability for Dynamic Parametric Processes, Reachability in Parameterized Systems: All Flavors of Threshold Automata, Unnamed Item, Fine-grained complexity of safety verification, Verification of Parameterized Communicating Automata via Split-Width, On the Complexity of Bounded Context Switching.

Cites Work

• Unnamed Item
• Subclasses of Presburger arithmetic and the polynomial-time hierarchy
• Verifying programs with unreliable channels
• The computational power of population protocols
• Verification of probabilistic systems with faulty communication
• Parameterised Pushdown Systems with Non-Atomic Writes
• Parameterized Verification of Asynchronous Shared-Memory Systems
• Parameterized Model Checking of Rendezvous Systems
• Reasoning about systems with many processes
• Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable
• Automated Deduction – CADE-20
• Reachability analysis of pushdown automata: Application to model-checking