Efficient algorithms for model checking pushdown systems
From MaRDI portal
Recommendations
Cited in
(69)- Note on winning positions on pushdown games with \(\omega\)-regular conditions
- Automatic verification of recursive procedures with one integer parameter.
- The complexity of bisimilarity-checking for one-counter processes.
- Analyzing pushdown systems with stack manipulation
- Model checking properties on reduced trace systems
- Eliminating the storage tape in reachability constructions.
- Model checking LTL with regular valuations for pushdown systems
- Pushdown module checking with imperfect information
- Detecting useless transitions in pushdown automata
- Reactive synthesis from visibly register pushdown automata
- Model checking interval temporal logics with regular expressions
- Operator precedence temporal logic and model checking
- Analyzing probabilistic pushdown automata
- Model checking dynamic pushdown networks
- Complexity results on branching-time pushdown model checking
- A generic framework for checking semantic equivalences between pushdown automata and finite-state automata
- Model checking for process rewrite systems and a class of action-based regular properties
- A ZDD-Based Efficient Higher-Order Model Checking Algorithm
- Automated formal analysis and verification: an overview
- Complexity results for prefix grammars
- Efficient CTL model-checking for pushdown systems
- Model checking procedural programs
- On the analysis of interacting pushdown systems
- Invariant Checking for Programs with Procedure Calls
- The Reachability Problem over Infinite Graphs
- Unary Automatic Graphs: An Algorithmic Perspective
- Complete SAT-Based Model Checking for Context-Free Processes
- An automata-theoretic approach to infinite-state systems
- Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending Chains
- Reducing behavioural to structural properties of programs with procedures
- Efficient CTL model-checking for pushdown systems
- scientific article; zbMATH DE number 1232241 (Why is no real title available?)
- scientific article; zbMATH DE number 1980931 (Why is no real title available?)
- Budget-bounded model-checking pushdown systems
- scientific article; zbMATH DE number 794257 (Why is no real title available?)
- Turing machines, transition systems, and interaction
- Model-checking bounded multi-pushdown systems
- scientific article; zbMATH DE number 7317259 (Why is no real title available?)
- CaRet with forgettable past
- Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-Vous
- On the expressivity of linear recursion schemes
- A first-order complete temporal logic for structured context-free languages
- Average stack cost of Büchi pushdown automata
- SMT-based model checking for recursive programs
- Program Analysis Using Weighted Pushdown Systems
- Efficient analysis of probabilistic programs with an unbounded counter
- scientific article; zbMATH DE number 2242594 (Why is no real title available?)
- Detecting useless transitions in pushdown automata
- Reachability analysis of pushdown systems with an upper stack
- Improving Pushdown System Model Checking
- Model-Checking HyperLTL for Pushdown Systems
- A Branching Time Variant of CaRet
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
- Relational Methods in Computer Science
- Reachability analysis of pushdown automata: Application to model-checking
- Verification of programs with exceptions through operator precedence automata
- LTL model checking of self modifying code
- The complexity gap in the static analysis of cache accesses grows if procedure calls are added
- Branching Temporal Logic of Calls and Returns for Pushdown Systems
- Reachability Analysis of Self Modifying Code
- Backwards-reachability for cooperating multi-pushdown systems
- Turing machines, transition systems, and interaction
- Reachability problems on reliable and lossy queue automata
- Model-checking structured context-free languages
- Summarization for termination: No return!
- Decidability issues for extended ping-pong protocols
- Compositional verification of sequential programs with procedures
- Verification and falsification of programs with loops using predicate abstraction
This page was built for publication: Efficient algorithms for model checking pushdown systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2754086)
