Practical CTL* model checking: Should SPIN be extended?

DOI10.1007/s100090050042zbMath1059.68591OpenAlexW1979424379MaRDI QIDQ1856161

Willem Visser, Howard Barringer

Publication date: 2000

Published in: International Journal on Software Tools for Technology Transfer. STTT (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s100090050042

zbMATH Keywords

model checkingBüchi automatagamesSPINhesitant alternating automata

Mathematics Subject Classification ID

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

Related Items (6)

On decidability properties of local sentences ⋮ A CTL* Model Checker for Petri Nets ⋮ CTL model checking on a shared-memory architecture ⋮ Linear temporal logic symbolic model checking ⋮ An Automata-Theoretic Approach to Infinite-State Systems ⋮ Automatically verifying temporal properties of pointer programs with cyclic proof

Uses Software

• CESAR

This page was built for publication: Practical CTL* model checking: Should SPIN be extended?