Budget-bounded model-checking pushdown systems

DOI10.1007/S10703-014-0207-YMaRDI QIDQ479843zbMATH OpenOpenAlexFDO

Authors Parosh A. Abdulla, Mohamed Faouzi Atig, Othmane Rezine, Jari Stenman

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

concurrent pushdown systemsLTL-model-checkingreachability problemrecursive programsverification problems

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)

Recommendations

• Reachability of scope-bounded multistack pushdown systems
• Model-checking bounded multi-pushdown systems
• Reachability of multistack pushdown systems with scope-bounded matching relations
• scientific article; zbMATH DE number 1670780
• Efficient CTL model-checking for pushdown systems

Cites work

• Adjacent ordered multi-pushdown systems
• Computer science today. Recent trends and developments
• CONCUR 2005 – Concurrency Theory
• Delay-bounded scheduling
• Emptiness of Multi-pushdown Automata Is 2ETIME-Complete
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 3497806 (Why is no real title available?)
• scientific article; zbMATH DE number 3509706 (Why is no real title available?)
• scientific article; zbMATH DE number 3639163 (Why is no real title available?)
• Linear-time model-checking for multithreaded programs under scope-bounding
• Model Checking Multithreaded Programs with Asynchronous Atomic Methods
• MULTI-PUSH-DOWN LANGUAGES AND GRAMMARS
• Reachability analysis of pushdown automata: Application to model-checking
• Reachability of multistack pushdown systems with scope-bounded matching relations
• Reducing concurrent analysis under a context bound to sequential analysis
• Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
• Reducing Context-Bounded Concurrent Reachability to Sequential Reachability
• Reversal-Bounded Counter Machines Revisited
• Scope-bounded multistack pushdown systems: fixed-point, sequentialization, and tree-width
• Summarizing procedures in concurrent programs
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(5)

• Reachability of scope-bounded multistack pushdown systems
• Context-free ambiguity detection using multi-stack pushdown automata
• A perfect model for bounded verification
• Data multi-pushdown automata
• Scope-bounded pushdown languages

Describes a project that uses

Uses Software

• CBMC
• ESBMC

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

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