Structural Invariants for the Verification of Systems with Parameterized Architectures

DOI10.1007/978-3-030-45190-5_13MaRDI QIDQ5039511zbMATH OpenFDO

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

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)

Cites work

• All for the price of few (parameterized verification through view abstraction)
• An SMT-based approach to coverability analysis
• Analyzing guarded protocols: better cutoffs, more systems, more expressivity
• Approaching the coverability problem continuously
• Automata theory and its applications
• Checking deadlock-freedom of parametric component-based systems
• Computer Aided Verification
• Decidability of parameterized verification
• scientific article; zbMATH DE number 1614699 (Why is no real title available?)
• scientific article; zbMATH DE number 1670768 (Why is no real title available?)
• scientific article; zbMATH DE number 1701752 (Why is no real title available?)
• scientific article; zbMATH DE number 1232242 (Why is no real title available?)
• scientific article; zbMATH DE number 1538040 (Why is no real title available?)
• Iterating transducers
• Parameterized model checking of rendezvous systems
• Reasoning about networks with many identical finite state processes
• Reasoning about systems with many processes
• Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
• Structural Invariants for the Verification of Systems with Parameterized Architectures
• Structural properties of petri nets
• Symbolic model checking with rich assertional languages
• Systematic design of program transformation frameworks by abstract interpretation
• Termination detection for diffusing computations
• Tight cutoffs for guarded protocols with fairness
• Verification, Model Checking, and Abstract Interpretation
• Well-structured transition systems everywhere!

Cited in

(11)

• Checking deadlock-freedom of parametric component-based systems
• Lifted structural invariant analysis of Petri net product lines
• Computing parameterized invariants of parameterized Petri nets
• Verification of component-based systems with recursive architectures
• Structural Invariants for the Verification of Systems with Parameterized Architectures
• Computing Parameterized Invariants of Parameterized Petri Nets
• Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure
• Modelling Uncertainty in Architectures of Parametric Component-Based Systems
• Minimal generating sets for semiflows
• Abduction of trap invariants in parameterized systems
• Regular model checking upside-down: an invariant-based approach

Describes a project that uses

Uses Software

• MONA
• D-Finder
• Cubicle

This page was built for publication: Structural Invariants for the Verification of Systems with Parameterized Architectures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5039511)