Naoki Kobayashi (the University of Tokyo)
On Two Higher-Order Extensions of Model Checking
Inspired by the success of finite state model checking in system verification, two kinds of its higher-order extensions have been studied since around 2000. One is model checking of higher-order recursion schemes (HORS), where the language for describing systems to be verified is extended to higher-order, and the other is higher-order fixpoint modal logic (HFL) model checking of finite-state systems, where the logic for specifying properties to be verified is extended to higher-order. The former has been successfully applied to automated verification of higher-order programs. In this talk, I will provide a gentle introduction to the HORS and HFL model checking problems, their applications to software verification, and the state-of-the-art of higher-order model checkers and tools built on top of them. I will also touch upon our recent result on the relationship between HORS and HFL model checking.
Naoki Kobayashi was born in 1968, and received his B.S., M.S., and D.S. degrees from the University of Tokyo in 1991, 1993 and 1996, respectively. He is currently a professor in Department of Computer Science, Graduate School of Information Science and Technology, The University of Tokyo. His current major research interests are in principles of programming languages, especially type systems, higher-order model checking, and program verification.