Types and Recursion Schemes for Higher-Order Program Verification Seminars/Workshops

Abstract

Higher-order recursion schemes (recursion schemes, for short) are expressive grammars for describing infinite trees. The modal µ-calculus model checking problem for recursion schemes (“Given a recursion scheme G and a modal µ-calculus formula phi, does the tree generated by G satisfy phi?”) has been a hot research topic in the theoretical community for recent years. In 2006, it has been shown to be decidable, and n-EXPTIME complete (where n is the order of a recursion scheme) by Ong.

The model checking of recursion schemes has recently turned out to be a good basis for verification of higher-order functional programs, just as finite state model checking for programs with while-loops, and pushdown model checking for programs with first-order recursion. First, various program analysis/verification problems such as reachability, flow analysis, and resource usage verification (or equivalently, type-state checking) can be easily transformed into model-checking problems for recursion schemes. Combined with a model checking algorithm for recursion schemes, this yields a sound, complete, and automated verification method for the simply-typed λ-calculus with recursion and finite base types such as booleans. Secondly, despite the extremely high worst-case time complexity (i.e. n-EXPTIME completeness) of the model checking problem for recursion schemes, our type-based model-checking algorithm turned out to run reasonably fast for realistic programs. We have implemented a prototype model checker for recursion schemes TRecS, and are currently working to construct a software model checker for a subset of ML on top of it.

The talk will summarize our recent results on the model checking of recursion schemes as well as its applications to higher-order program verification, and discuss future perspectives.