Efficient CTL model-checking for pushdown systems

DOI10.1016/J.TCS.2014.07.001zbMATH Open1360.68599OpenAlexW2020438328MaRDI QIDQ402129FDOQ402129

Fu Song, Tayssir Touili

Publication date: 27 August 2014

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2014.07.001

Recommendations

• Efficient CTL model-checking for pushdown systems
• scientific article; zbMATH DE number 2080197
• scientific article; zbMATH DE number 1670780
• Model-Checking HyperLTL for Pushdown Systems
• Improving Pushdown System Model Checking
• Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
• Model-checking bounded multi-pushdown systems

zbMATH Keywords

CTLmodel-checkingCTL with regular valuationspushdown system

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cites Work

• A lattice-theoretical fixpoint theorem and its applications
• Title not available (Why is that?)
• Reachability analysis of pushdown automata: Application to model-checking
• Pushdown module checking
• Title not available (Why is that?)
• Model checking LTL with regular valuations for pushdown systems
• Complexity results on branching-time pushdown model checking
• Title not available (Why is that?)
• Note on winning positions on pushdown games with \(\omega\)-regular conditions
• Deciding emptiness for stack automata on infinite trees
• Title not available (Why is that?)
• Uniform solution of parity games on prefix-recognizable graphs
• Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains
• An Automata-Theoretic Approach to Infinite-State Systems
• Title not available (Why is that?)
• Model checking the full modal mu-calculus for infinite sequential processes
• Title not available (Why is that?)
• Title not available (Why is that?)
• Computer Aided Verification
• A saturation method for the modal \(\mu \)-calculus over pushdown systems
• Pushdown Module Checking
• Title not available (Why is that?)

Cited In (14)

• Not all bugs are created equal, but robust reachability can tell the difference
• Improving Pushdown System Model Checking
• Model-Checking HyperLTL for Pushdown Systems
• Branching Temporal Logic of Calls and Returns for Pushdown Systems
• Model checking LTL with regular valuations for pushdown systems
• A Branching Time Variant of CaRet
• Introducing robust reachability
• Title not available (Why is that?)
• Practical CTL* model checking: Should SPIN be extended?
• Title not available (Why is that?)
• Analyzing pushdown systems with stack manipulation
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Uses Software

• PuMoC

This page was built for publication: Efficient CTL model-checking for pushdown systems

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