Be lazy and don't care: faster CTL model checking for recursive state machines

DOI10.1007/978-3-030-92124-8_19zbMath1522.68311OpenAlexW4205115130MaRDI QIDQ6045062

Ansgar Fehnker, Patrick Wienhöft, Clemens Dubslaff

Publication date: 26 May 2023

Published in: Software Engineering and Formal Methods (Search for Journal in Brave)

Full work available at URL: https://research.utwente.nl/en/publications/15127c0e-2afb-4b6a-97b4-acf4b31eb220

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A saturation method for the modal \(\mu \)-calculus over pushdown systems
• Model checking the full modal mu-calculus for infinite sequential processes
• Weighted pushdown systems and their application to interprocedural dataflow analysis
• Model Checking Procedural Programs
• Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations
• Graph-Based Algorithms for Boolean Function Manipulation
• Interprocedural Analysis with Lazy Propagation
• Reachability analysis of pushdown automata: Application to model-checking

This page was built for publication: Be lazy and don't care: faster CTL model checking for recursive state machines