Automatic verification of parameterized networks of processes

DOI10.1016/S0304-3975(00)00104-3zbMath0973.68145OpenAlexW2023327000MaRDI QIDQ5941103

No author found.

Publication date: 20 August 2001

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(00)00104-3

zbMATH Keywords

model-checkingparameterized networkssynchronous observerswidening

Mathematics Subject Classification ID

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

Related Items (14)

Compositional analysis for verification of parameterized systems ⋮ Model checking and abstraction to the aid of parameterized systems (a survey) ⋮ Model Checking Parameterized Systems ⋮ Parametrized invariance for infinite state processes ⋮ An automatic abstraction technique for verifying featured, parameterised systems ⋮ Networks of Processes with Parameterized State Space ⋮ Symbolic model checking with rich assertional languages ⋮ Automatic verification of parameterized networks of processes ⋮ Verifying Parameterized taDOM+ Lock Managers ⋮ Liveness by Invisible Invariants ⋮ On Verifying Fault Tolerance of Distributed Protocols ⋮ Network invariants for real-time systems ⋮ Quantitative static analysis of communication protocols using abstract Markov chains ⋮ Automated formal analysis and verification: an overview

Uses Software

• CESAR
• LUSTRE
• Esterel

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Distributed mutual exclusion on a ring of processes
• The Esterel synchronous programming language: Design, semantics, implementation
• An experience in proving regular networks of processes by modular model checking
• A structural induction theorem for processes
• Grammar Analysis and Parsing by Abstract Interpretation
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Abstract interpretation and application to logic programs
• On Reasoning About Rings
• Symbolic model checking with rich assertional languages
• Automatic verification of parameterized networks of processes

This page was built for publication: Automatic verification of parameterized networks of processes