Automatic WSTS-based repair and deadlock detection of parameterized systems

DOI10.1007/S10703-025-00469-2MaRDI QIDQ6913625zbMATH OpenFDO

Authors Swen Jacobs, Mouhammad Sakr, Marcus Völp

Publication date 21 October 2025

Published in Formal Methods in System Design (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10703-025-00469-2

zbMATH Keywords

deadlock detectionparameterized model checkingparameterized repairwell-structured transition systems

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)

Cites work

• Abstraction-guided synthesis of synchronization
• Analyzing guarded protocols: better cutoffs, more systems, more expressivity
• Assume, guarantee or repair
• Complexity analysis of the backward coverability algorithm for VASS
• Computer Aided Verification
• CONCUR 2004 - Concurrency Theory
• Decidability of parameterized verification
• Exact and efficient verification of parameterized cache coherence protocols
• Handbook of model checking
• scientific article; zbMATH DE number 1614699 (Why is no real title available?)
• scientific article; zbMATH DE number 2080048 (Why is no real title available?)
• scientific article; zbMATH DE number 1903348 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Keeping a crowd safe: on the complexity of parameterized verification (invited talk)
• Lazy synthesis
• Model checking of safety properties
• Model checking parameterised multi-token systems via the composition method
• On Reasoning About Rings
• Parameterized Analysis of Immediate Observation Petri Nets
• Parameterized model checking of rendezvous systems
• Parameterized Model Checking of Token-Passing Systems
• Parameterized verification of ad hoc networks
• Parameterized verification of systems with global synchronization and guards
• Proving properties of a ring of finite-state machines
• Reasoning about systems with many processes
• Reduction and covering of infinite reachability trees
• Repair of Boolean Programs with an Application to C
• Stabilization, safety, and security of distributed systems. 9th international symposium, SSS 2007 Paris, France, November 14--16, 2007. Proceedings
• Symbolic Counter Abstraction for Concurrent Software
• Synchronization synthesis for network programs
• The complexity of reachability in affine vector addition systems with states
• The power of well-structured systems
• The reachability problem for Petri nets is not primitive recursive
• Tight cutoffs for guarded protocols with fairness
• Well-structured transition systems everywhere!

This page was built for publication: Automatic WSTS-based repair and deadlock detection of parameterized systems

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