Write a Blog >>
Mon 18 Jan 2016 08:30 - 10:00 at Room HTC 3 - T5: Higher-Order Model Checking
Mon 18 Jan 2016 16:00 - 17:30 at Room HTC 3 - T5: 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 90 minutes, given twice at 8:30-10:00, and 16:00-17:30.

Mon 18 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

08:30 - 10:00
T5: Higher-Order Model CheckingTutorials at Room HTC 3
08:30
90m
Talk
T5: Higher-Order Model Checking
Tutorials
Naoki Kobayashi University of Tokyo, C.-H. Luke Ong University of Oxford, UK
16:00 - 17:30
T5: Higher-Order Model CheckingTutorials at Room HTC 3
16:00
90m
Talk
T5: Higher-Order Model Checking
Tutorials
Naoki Kobayashi University of Tokyo, C.-H. Luke Ong University of Oxford, UK