POPL 2016 Tutorial: Higher-Order Model Checking
Higher-order model checking is a generalization of finite-state model
checking, obtained by replacing finite-state models with more
expressive models called higher-order recursion schemes (HORS). From a
programming language perspective, HORS may be viewed as a simply-typed
functional program for generating an infinite tree, and higher-order
model checking is concerned with checking properties of the tree
generated by HORS. Higher-order model checking is an interesting and
challenging topic from both theoretical and practical perspectives. On
the theoretical side, it has rich theories, with connections to
various topics of theoretical computer science, including λ-calculus,
type theories (intersection types, in particular), game semantics, and
formal languages/automata theory. On the practical side, it enables
fully automated verification of higher-order programs.
The tutorial will start with a gentle introduction to higher-order
model checking and its historical background, and cover both theories
and applications of higher-order model checking, with an emphasis on
applications to program verification.
The tutorial consists of four parts:
- Part 1: Introduction (by Ong)
- Part 2: Applications to Program Verification (by Kobayashi)
- Part 3: Type Systems and Algorithms for Higher-Order Model Checking (by Kobayashi)
- Part 4: Advanced Materials (by Ong)
Slides