Reachability of scope-bounded multistack pushdown systems

DOI10.1016/j.ic.2020.104588zbMath1496.68235OpenAlexW2965450052MaRDI QIDQ2216111

Salvatore La Torre, Margherita Napoli, Gennaro Parlato

Publication date: 15 December 2020

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2020.104588

zbMATH Keywords

verificationreachabilitymultistack pushdown automata

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 (1)

Recent advances on reachability problems for valence systems (invited talk)

Cites Work

• Unnamed Item
• Temporal logics for concurrent recursive programs: satisfiability and model checking
• Budget-bounded model-checking pushdown systems
• Computer aided verification. 22nd international conference, CAV 2010, Edinburgh, UK, July 15--19, 2010. Proceedings
• Computer aided verification. 21st international conference, CAV 2009, Grenoble, France, June 26--July 2, 2009. Proceedings
• Stateless model checking for TSO and PSO
• Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
• MSO Decidability of Multi-Pushdown Systems via Split-Width
• A Temporal Logic for Multi-threaded Programs
• A Unifying Approach for Multistack Pushdown Automata
• Scope-bounded multistack pushdown systems: fixed-point, sequentialization, and tree-width
• Saturation of Concurrent Collapsible Pushdown Systems
• Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations
• Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
• An Infinite Automaton Characterization of Double Exponential Time
• Games on Multi-stack Pushdown Systems
• Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads
• On the Expressive Power of 2-Stack Visibly Pushdown Automata
• Reducing Context-Bounded Concurrent Reachability to Sequential Reachability
• Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding
• Model-Checking Bounded Multi-Pushdown Systems
• Bounded Context Switching for Valence Systems
• On the Complexity of Bounded Context Switching.
• ADJACENT ORDERED MULTI-PUSHDOWN SYSTEMS
• The Complexity of Model Checking Multi-stack Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Delay-bounded scheduling
• Decidable logics combining heap structures and data
• 2-Visibly Pushdown Automata
• Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures
• Interprocedural Analysis of Concurrent Programs Under a Context Bound
• Context-Bounded Analysis of Concurrent Queue Systems
• MULTI-PUSH-DOWN LANGUAGES AND GRAMMARS
• Tools and Algorithms for the Construction and Analysis of Systems
• Scope-Bounded Pushdown Languages

This page was built for publication: Reachability of scope-bounded multistack pushdown systems