From pre-historic to post-modern symbolic model checking

DOI10.1023/A:1026228213080zbMath1074.68036OpenAlexW1607643415MaRDI QIDQ1878908

Shaz Qadeer, Orna Kupferman, Thomas A. Henzinger

Publication date: 9 September 2004

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1026228213080

zbMATH Keywords

symbolic model checking\(\mu\) calculus\(\omega\)-regular specificationsforward traversal

Mathematics Subject Classification ID

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

Related Items

Forward analysis and model checking for trace bounded WSTS, Symbolic Model Checking in Non-Boolean Domains, GSTE is partitioned model checking, Fine-grained complexity lower bounds for problems in computer aided verification, On relative and probabilistic finite counterability, Approximation Refinement for Interpolation-Based Model Checking, Expand, enlarge and check: new algorithms for the coverability problem of WSTS

Uses Software

• SPIN
• CESAR