TRecS

TRecS: A type-based model checker for recursion schemes. TRecS is a model checker for higher-order recursion schemes, which takes a higher-order recursion scheme G and a (deterministic) trivial automaton A as input, and checks whether the (possibly infinite) tree generated by G is accepted by A. The model checking problem for higher-order recursion schemes has been shown to be decidable by Luke Ong in 2006, but its worst-case complexity is k-EXPTIME complete for order-k recursion schemes. TRecS is (to our knowledge) the first implementation of a higher-order model checker ever built. It uses a type-based model checking algorithm proposed by Kobayashi at PPDP 2009, and runs fast for many typical inputs, despite the huge worst-case complexity. Since the development of TRecS, it has been used as backends of program verification tools, like MoCHi, which is a sort of ”software model checker” for ML, and EHMTT Verifier, which is also a verification tool for tree-generating functional programs. You can test TRecS through the web interface below. The technical background is found in: Naoki Kobayashi, Model Checking Higher-Order Programs, JACM, 60(3), 2013.