THORS (Types for Higher-Order Recursion Schemes)
Abstract from Technical Report
Recent advances in the model checking of recursion schemes have opened the prospect of a model checking approach to the verification of higher-order functional programs. We formulate the Resource Usage Verification Problem in a general (liveness) setting, where good behaviours are specified by alternating parity (word) automata; and we give a sound and complete decision procedure by reduction to the problem of model checking higher-order recursion schemes (HORS) against alternating parity tree automata. Extending Kobayashi's type-inference approach, we present an efficient algorithm for deciding a restriction of the model checking problem in which properties are expressed by alternating weak tree automata (and hence all CTL formulas). We have constructed a model checker, THORS, that implements our algorithm and a number of optimisations. Despite the hugely challenging worst-case time complexity, THORS performs remarkably well on small examples, even up to order 5. To our knowledge, this is the first model checker for HORS which allows for the specification of tree automata with a non-trivial acceptance condition, including all CTL properties.
Web Interface
Here you can test THORS online. The web interface allows you to enter an input file for THORS to verify. To get an idea of the input format, look at the examples.