TravMC2: higher-order model checking for alternating parity tree automata. Higher-order model checking is the problem of model checking (possibly) infinite trees generated by higher-order recursion schemes (HORS). HORS are a natural abstract model of functional programs, and HORS model checkers play a similar role to checkers of Boolean programs in the imperative setting. Most research effort so far has focused on checking safety properties specified using trivial tree automata i.e. Buechi tree automata all of whose states are final. Building on our previous work, we present a higher-order model checker, TravMC2, which supports properties specified using alternating parity tree automata (or equivalently monadic second order logic). Our experimental results offer an encouraging comparison with an existing checker, TrecS-APT.
Keywords for this software
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Parys, Paweł: Recursion schemes, the MSO logic, and the \textsfUquantifier (2020)
- Parys, Paweł: Recursion schemes and the WMSO+U logic (2018)
- Suzuki, Ryota; Fujima, Koichi; Kobayashi, Naoki; Tsukada, Takeshi: Streett automata model checking of higher-order recursion schemes (2017)
- Watanabe, Keiichi; Sato, Ryosuke; Tsukada, Takeshi; Kobayashi, Naoki: Automatically disproving fair termination of higher-order functional programs (2016)