scientific article

Javier Esparza, Stefan Schwoon, D. Hansel, Peter Rossmanith

Publication date: 11 November 2001

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

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

Related Items (52)

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 ⋮ Model checking LTL with regular valuations for pushdown systems ⋮ Complexity results on branching-time pushdown model checking ⋮ Model Checking Procedural Programs ⋮ Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-Vous ⋮ Summarization for termination: No return! ⋮ Decidability issues for extended ping-pong protocols ⋮ A generic framework for checking semantic equivalences between pushdown automata and finite-state automata ⋮ Reducing behavioural to structural properties of programs with procedures ⋮ Model checking interval temporal logics with regular expressions ⋮ Verification of programs with exceptions through operator precedence automata ⋮ 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 ⋮ Automatic verification of recursive procedures with one integer parameter. ⋮ The complexity of bisimilarity-checking for one-counter processes. ⋮ Complete SAT-Based Model Checking for Context-Free Processes ⋮ Branching Temporal Logic of Calls and Returns for Pushdown Systems ⋮ Reachability Analysis of Self Modifying Code ⋮ Analyzing pushdown systems with stack manipulation ⋮ Operator precedence temporal logic and model checking ⋮ Compositional verification of sequential programs with procedures ⋮ Model checking properties on reduced trace systems ⋮ SMT-based model checking for recursive programs ⋮ Analyzing probabilistic pushdown automata ⋮ Turing Machines, Transition Systems, and Interaction ⋮ Complexity results for prefix grammars ⋮ Detecting Useless Transitions in Pushdown Automata ⋮ Reachability Analysis of Pushdown Systems with an Upper Stack ⋮ Verification and falsification of programs with loops using predicate abstraction ⋮ Turing machines, transition systems, and interaction ⋮ An Automata-Theoretic Approach to Infinite-State Systems ⋮ Model checking for process rewrite systems and a class of action-based regular properties ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending Chains ⋮ Program Analysis Using Weighted Pushdown Systems ⋮ Detecting useless transitions in pushdown automata ⋮ Note on winning positions on pushdown games with \(\omega\)-regular conditions ⋮ Efficient CTL Model-Checking for Pushdown Systems ⋮ Invariant Checking for Programs with Procedure Calls ⋮ The Reachability Problem over Infinite Graphs ⋮ CaRet With Forgettable Past ⋮ Efficient Analysis of Probabilistic Programs with an Unbounded Counter ⋮ Automated formal analysis and verification: an overview ⋮ Model checking dynamic pushdown networks

Uses Software

MONA

This page was built for publication: