Types and recursion schemes for higher-order program verification

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 φ, does the tree generated by G satisfy φ?") has been a hot research topic in the theoretical community for recent years [1,2,3,4,5,6,7]. In 2006, it has been shown to be decidable, and n-EXPTIME complete (where n is the order of a recursion scheme) by Ong [5]. 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 [8]. 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 [9] 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 [8,9,10,11] on the model checking of recursion schemes as well as its applications to higher-order program verification, and discuss future perspectives. © 2009 Springer-Verlag.