Model checking and abstraction to the aid of parameterized systems (a survey)

DOI10.1016/j.cl.2004.02.006zbMath1072.68069OpenAlexW1967917857MaRDI QIDQ1886449

Lenore D. Zuck, Amir Pnueli

Publication date: 18 November 2004

Published in: Computer Languages, Systems \& Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.cl.2004.02.006

zbMATH Keywords

LivenessSafetyCounter abstractionInvisible invariantsInvisible rankingParameterized systemsProbabilistic verificationProgress

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)

Related Items (9)

A counter abstraction technique for verifying properties of probabilistic swarm systems ⋮ Directed reachability for infinite-state systems ⋮ Parametrized invariance for infinite state processes ⋮ Parameterized model checking of networks of timed automata with Boolean guards ⋮ Proving the Refuted: Symbolic Model Checkers as Proof Generators ⋮ Liveness by Invisible Invariants ⋮ Model Checking for Action Abstraction ⋮ Towards a Thread-Local Proof Technique for Starvation Freedom ⋮ Parameterised verification for multi-agent systems

Uses Software

• PRISM
• MONA
• Cadence SMV
• STeP

Cites Work

• An approach to automating the verification of compact parallel coordination programs. I
• The choice coordination problem
• Fairness and related properties in transition systems - a temporal logic to deal with fairness
• An experience in proving regular networks of processes by modular model checking
• Symmetric and economical solutions to the mutual exclusion problem in a distributed system
• Probabilistic verification
• Control and data abstraction: The cornerstones of practical formal verification
• A structural induction theorem for processes
• Reasoning about systems with many processes
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation
• Symbolic model checking with rich assertional languages
• Automatic verification of parameterized networks of processes
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Model checking and abstraction to the aid of parameterized systems (a survey)