scientific article; zbMATH DE number 1796143

zbMath0991.68539MaRDI QIDQ4551162

Javier Esparza, Stefan Schwoon

Publication date: 4 September 2002

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2102/21020324

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

A Branching Time Variant of CaRet ⋮ Model checking LTL with regular valuations for pushdown systems ⋮ Model Checking Procedural Programs ⋮ Model Checking Concurrent Programs ⋮ Summarization for termination: No return! ⋮ Faster pushdown reachability analysis with applications in network verification ⋮ A generic framework for checking semantic equivalences between pushdown automata and finite-state automata ⋮ Unnamed Item ⋮ Regular model checking: evolution and perspectives ⋮ Verification of programs with exceptions through operator precedence automata ⋮ Efficient CTL model-checking for pushdown systems ⋮ Pushdown timed automata: A binary reachability characterization and safety verification. ⋮ Complete SAT-Based Model Checking for Context-Free Processes ⋮ A model checking-based approach for security policy verification of mobile systems ⋮ Analyzing pushdown systems with stack manipulation ⋮ Verifying parallel programs with dynamic communication structures ⋮ Multi-matching nested relations ⋮ Model Checking Recursive Programs with Exact Predicate Abstraction ⋮ Verification of Boolean programs with unbounded thread creation ⋮ An Automata-Theoretic Approach to Infinite-State Systems ⋮ On the complexity of checking semantic equivalences between pushdown processes and finite-state processes ⋮ Efficient CTL Model-Checking for Pushdown Systems ⋮ Verifying Parallel Programs with Dynamic Communication Structures

Uses Software

• FoCs