Reachability analysis of pushdown automata: Application to model-checking

DOI10.1007/3-540-63141-0_10zbMath1512.68135OpenAlexW1589224558MaRDI QIDQ6044114

Javier Esparza, Ahmed Bouajjani, Oded Maler

Publication date: 17 May 2023

Published in: CONCUR '97: Concurrency Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-63141-0_10

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Reactive synthesis from visibly register pushdown automata, Eliminating the storage tape in reachability constructions., Model-Checking HyperLTL for Pushdown Systems, A Branching Time Variant of CaRet, Reachability problems on reliable and lossy queue automata, Model-checking structured context-free languages, Modular strategies for recursive game graphs, Model checking LTL with regular valuations for pushdown systems, An Approach to Computing Downward Closures, Complexity results on branching-time pushdown model checking, SAT-Based Model Checking, Model Checking Procedural Programs, Model Checking Concurrent Programs, An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics, Faster pushdown reachability analysis with applications in network verification, Expression-Based Aliasing for OO–languages, Ordered multi-stack visibly pushdown automata, Reachability in pushdown register automata, Permutation rewriting and algorithmic verification, Symbolic weighted language models, quantitative parsing and automated music transcription, A generic framework for checking semantic equivalences between pushdown automata and finite-state automata, Branching-time logics with path relativisation, On store languages and applications, Regular model checking: evolution and perspectives, Be lazy and don't care: faster CTL model checking for recursive state machines, On monitoring linear temporal properties, Efficient CTL model-checking for pushdown systems, Unary Automatic Graphs: An Algorithmic Perspective, LTL model checking of self modifying code, The complexity gap in the static analysis of cache accesses grows if procedure calls are added, Interval Temporal Logic for Visibly Pushdown Systems, Verification in loosely synchronous queue-connected discrete timed automata., Automatic verification of recursive procedures with one integer parameter., Pushdown timed automata: A binary reachability characterization and safety verification., Model checking of pushdown systems for projection temporal logic, The complexity of bisimilarity-checking for one-counter processes., Improved model checking of hierarchical systems, Complete SAT-Based Model Checking for Context-Free Processes, Branching Temporal Logic of Calls and Returns for Pushdown Systems, The Birth of Model Checking, Reachability Analysis of Self Modifying Code, Unnamed Item, Analyzing pushdown systems with stack manipulation, Unnamed Item, Verifying parallel programs with dynamic communication structures, Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations, Emptiness of Multi-pushdown Automata Is 2ETIME-Complete, When Is Reachability Intrinsically Decidable?, Operator precedence temporal logic and model checking, Past pushdown timed automata and safety verification., Reachability in recursive Markov decision processes, Model checking parameterized asynchronous shared-memory systems, An efficient automata approach to some problems on context-free grammars., Visibly rational expressions, Budget-bounded model-checking pushdown systems, Compositional verification of sequential programs with procedures, Emptiness of Ordered Multi-Pushdown Automata is 2ETIME-Complete, Efficient SAT-based bounded model checking for software verification, Analyzing probabilistic pushdown automata, Verification of qualitative \(\mathbb Z\) constraints, A saturation method for the modal \(\mu \)-calculus over pushdown systems, On Decidability of LTL+Past Model Checking for Process Rewrite Systems, Reachability on prefix-recognizable graphs, Decidability of model checking with the temporal logic EF, Deciding bisimulation-like equivalences with finite-state processes, Unnamed Item, Decidable models of integer-manipulating programs with recursive parallelism, Unnamed Item, Model checking for process rewrite systems and a class of action-based regular properties, Unnamed Item, Visibly linear dynamic logic, Parameterized verification of coverability in infinite state broadcast networks, Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time, The regular viewpoint on PA-processes, Tight bounds for reachability problems on one-counter and pushdown systems, Unnamed Item, Interprocedural Analysis of Concurrent Programs Under a Context Bound, Program Analysis Using Weighted Pushdown Systems, Detecting useless transitions in pushdown automata, Shortest Paths in One-Counter Systems, CaRet With Forgettable Past, Model-Checking Counting Temporal Logics on Flat Structures, Domains for Higher-Order Games, Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations, Counter machines and verification problems., Process rewrite systems., Context-free timed formalisms: robust automata and linear temporal logics, Model checking dynamic pushdown networks

Cites Work