DIKU IT-C RUC

COPLAS

Copenhagen Programming Language Seminar

Type-Based Higher-Order Model Checking

Naoki Kobayashi, Tohoku University

Thursday, November 11th, 2010
DIKU, Universitetsparken 1, 14:00-15:00, Meeting room A+B

Abstract:
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.


Bio:

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

Scientific host: Fritz Heinglein Administrative host:Jette Møller. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org