Model checking parameterized asynchronous shared-memory systems

DOI10.1007/s10703-016-0258-3zbMath1360.68584arXiv1505.06588MaRDI 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 checking; shared-memory systems; parametrized verification

Mathematics Subject Classification ID

68Q25: Analysis of algorithms and problem complexity

68Q45: Formal languages and automata

68Q60: Specification and verification (program logics, model checking, etc.)

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

Related Items

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

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