TRecS 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 all top 5 Cited by 6 Authors 1 Kobayashi, Naoki 1 Neatherway, Robin P. 1 Ong, Chih-Hao Luke 1 Ramsay, Steven James 1 Tobita, Yoshihiro 1 Tsukada, Takeshi Cited in 0 Serials Cited in 1 Field 2 Computer science (68-XX) Citations by Year