Budget-bounded model-checking pushdown systems

DOI10.1007/s10703-014-0207-yzbMath1317.68106OpenAlexW1996831638MaRDI QIDQ479843

Mohamed Faouzi Atig, Jari Stenman, Parosh Aziz Abdulla, Othmane Rezine

Publication date: 5 December 2014

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

Full work available at URL: https://doi.org/10.1007/s10703-014-0207-y

zbMATH Keywords

verification problemsreachability problemrecursive programsconcurrent pushdown systemsLTL-model-checking

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) 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 (4)

Reachability of scope-bounded multistack pushdown systems ⋮ Scope-Bounded Pushdown Languages ⋮ Context-Free Ambiguity Detection Using Multi-stack Pushdown Automata ⋮ Data Multi-Pushdown Automata

Uses Software

• CBMC
• ESBMC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reducing concurrent analysis under a context bound to sequential analysis
• Computer science today. Recent trends and developments
• Scope-bounded multistack pushdown systems: fixed-point, sequentialization, and tree-width
• Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations
• Summarizing procedures in concurrent programs
• Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
• Emptiness of Multi-pushdown Automata Is 2ETIME-Complete
• Reversal-Bounded Counter Machines Revisited
• Reducing Context-Bounded Concurrent Reachability to Sequential Reachability
• Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding
• Adjacent Ordered Multi-Pushdown Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Delay-bounded scheduling
• MULTI-PUSH-DOWN LANGUAGES AND GRAMMARS
• Tools and Algorithms for the Construction and Analysis of Systems
• Model Checking Multithreaded Programs with Asynchronous Atomic Methods
• CONCUR 2005 – Concurrency Theory
• Tools and Algorithms for the Construction and Analysis of Systems
• Reachability analysis of pushdown automata: Application to model-checking

This page was built for publication: Budget-bounded model-checking pushdown systems