Model-checking parametric lock-sharing systems against regular constraints

DOI10.4230/LIPICS.CONCUR.2023.24MaRDI QIDQ6967323zbMATH OpenFDO

Authors Corto N. Mascle, Anca Muscholl, Igor Walukiewicz

Publication date 26 June 2025

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.CONCUR.2023.24

zbMATH Keywords

locksmodel-checkingparametric systems

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites work

• Computer Aided Verification
• CONCUR 2005 – Concurrency Theory
• Dealing with Priorities and Locks for Concurrent Programs
• Decidability of parameterized verification
• scientific article; zbMATH DE number 5954655 (Why is no real title available?)
• scientific article; zbMATH DE number 7682282 (Why is no real title available?)
• Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation
• Model checking parameterized systems
• Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems
• Parameterised pushdown systems with non-atomic writes
• Parameterized Verification of Asynchronous Shared-Memory Systems
• Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints
• Reachability analysis of pushdown automata: Application to model-checking
• Reachability for dynamic parametric processes
• Reachability of scope-bounded multistack pushdown systems
• Reasoning about systems with many processes
• Revisiting underapproximate reachability for multipushdown systems
• The complexity of bounded context switching with dynamic thread creation
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification of higher-order concurrent programs with dynamic resource creation

Cited in

(1)

• Constraint automata on infinite data trees: from \(\mathrm{CTL}(\mathbb{Z})/\mathrm{CTL}^*(\mathbb{Z})\) to decision procedures

This page was built for publication: Model-checking parametric lock-sharing systems against regular constraints

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