Type-Based Higher-Order Model Checking

COPLAS Talk by Naoki Kobayashi, Tohoku University 


We have recently proposed a new approach to automated verification of higher-order programs, where higher-order programs are first transformed into higher-order recursion schemes, and then model-checked. This verification method is sound, complete, and fully automated for the simply-typed lambda calculus with recursion and finite data domains. A significant challenge to enable this approach is to develop an efficient model checking algorithm for higher-order recursion schemes. In the talk, we show that the model checking of higher-order recursion schemes can be reduced to a type checking problem for an intersection type system, and use this reduction to derive a practical model checking algorithm for higher-order recursion schemes. Based on the algorithm, we have developed TRecS, the first model checker for higher-order recursion schemes. Despite the extremely high worst-case complexity, TRecS is surprisingly fast for realistic inputs, and works well as a backend of our verification tools for functional programs. We also mention certain limitations of our model checking algorithm, and discuss ongoing and future work to overcome those limitations.

A part of this work has been done in collaboration with Luke Ong.

Naoki Kobayashi is a professor of Computer Science at Tohoku University. He received his PhD from University of Tokyo in 1996.
After working as a full-time lecturer at University of Tokyo (1996-2000), and an associate professor at Tokyo Institute of Technology (2001-2004), he moved to Tohoku University in 2004. His research interests are in principles of programming languages, in particular,
type systems, program verification, and concurrency.

Scientific host: Fritz Henglein, henglein@diku.dk
Administrative host: Jette Møller, jettegm@diku.dk