Structural Invariants for the Verification of Systems with Parameterized Architectures

DOI10.1007/978-3-030-45190-5_13MaRDI QIDQ5039511

Joseph Sifakis, Javier Esparza, Christoph Welzel, Marius Bozga, Radu Iosif

Publication date: 13 October 2022

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Structural Invariants for the Verification of Systems with Parameterized Architectures, Computing Parameterized Invariants of Parameterized Petri Nets, Modelling Uncertainty in Architectures of Parametric Component-Based Systems, Verification of component-based systems with recursive architectures, Checking deadlock-freedom of parametric component-based systems, Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure, Lifted structural invariant analysis of Petri net product lines, Computing parameterized invariants of parameterized Petri nets

Uses Software

• D-Finder
• MONA
• Cubicle

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reasoning about networks with many identical finite state processes
• Termination detection for diffusing computations
• Parameterized model checking of rendezvous systems
• Iterating transducers
• Checking deadlock-freedom of parametric component-based systems
• Approaching the coverability problem continuously
• Tight Cutoffs for Guarded Protocols with Fairness
• An SMT-Based Approach to Coverability Analysis
• All for the Price of Few
• Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity
• Structural properties of petri nets
• Reasoning about systems with many processes
• Decidability of Parameterized Verification
• Structural Invariants for the Verification of Systems with Parameterized Architectures
• Systematic design of program transformation frameworks by abstract interpretation
• Computer Aided Verification
• Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
• Verification, Model Checking, and Abstract Interpretation
• Automata theory and its applications
• Well-structured transition systems everywhere!
• Symbolic model checking with rich assertional languages