swMATH ID: 14145
Software Authors: Kobayashi, N.
Description: 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.
Homepage: http://www.kb.ecei.tohoku.ac.jp/~koba/trecs/
Related Software: TravMC; BLAST; THORS; EigenCFA
Cited in: 2 Publications

Cited in 0 Serials

Citations by Year