### Luke Ong

Dept. of Computer Science

University of Oxford

United Kingdom

## Higher-Order Model Checking

#### Abstract

This course is about the foundations and algorithms that underpin recent developments in the model checking of higher-order programs.

We begin by studying two models of higher-order computation: recursion schemes and collapsible pushdown automata.

Recursion schemes are in essence the simply-typed λ-calculus with recursion, generated from first-order symbols.

Collapsible pushdown automata are a generalisation of pushdown automata to higher-order stacks - which are iterations of stacks of stacks - that contain symbols equipped with links.

We study and compare the expressive power of the two models and the algorithmic properties of infinite structures such as trees and graphs generated by them.

We survey applications to the verification of higher-order functional programs, focussing on recent developments of "practical" algorithms.

A central theme is the fruitful interplay of ideas between the neighbouring fields of semantics and algorithmic verification.

#### Course materials

- L. Ong. Higher-order model checking. EWSCS 2013 course slides. Part 1 (lectures 1-2) [pdf], part 2 (lectures 2-3) [pdf], parts 3-4 (lecture 4) [pdf]
- Videos from the lectures.
- L. Ong. Recursion schemes, collapsible automata and higher-order model checking. Manuscript. [pdf]
- L. Ong. Automata, logic and games. University of Oxford lecture notes, 2013.
- W. Blum, L. Ong. The safe lambda calculus.
*Logical Methods in Computer Science*, v. 5, n. 1, article 3, 2009. [doi link] - L. Ong. On model-checking trees generated by higher-order
recursion schemes. In
*Proc. of LICS 2006*, pp. 81-90. IEEE CS, 2006. [doi link]. - N. Kobayashi, L. Ong. Complexity of model checking recursion
schemes for fragments of the modal mu-calculus.
*Logical Methods in Computer Science*, v. 7, n. 4, article 9, 2011. [doi link] - C. Broadbent, A. Carayol, L. Ong, O. Serre. Recursion schemes and
logical reflection. In
*Proc. of LICS 2010*, pp. 120-129. IEEE CS, 2010. [doi link] - C. Broadbent, L. Ong. On global model checking trees generated by
higher-order recursion schemes. In
*Proc. of FoSSaCS 2009*, v. 5504 of Lect. Notes in Comput. Sci., pp. 107-121. Springer, 2009. [doi link] - N. Kobayashi, L. Ong. A type system equivalent to modal
mu-calculus model checking of recursion schemes. In
*Proc. of LICS 2009*, pp. 179-188. IEEE CS, 2009. [doi link] - M. Hague, A. S. Murawski, L. Ong, O. Serre. Collapsible pushdown
automata and recursion schemes. In
*Proc. of LICS 2008*, pp. 452-461. IEEE CS, 2008. [doi link] - A. Carayol, M. Hague, A. Meyer, L. Ong, O. Serre. Winning regions
of higher-order pushdown games. In
*Proc. of LICS 2008*, pp. 193-204. IEEE CS, 2008. [doi link] - L. Ong, T. Tsukada. Two-level game semantics, intersection types,
and recursion schemes. In
*Proc. of ICALP 2012, Part 2*, v. 7392 of*Lect. Notes in Comput. Sci.*, pp. 325-336. Springer, 2012. [doi link] - R. P. Neatherway, L. Ong, S. J. Ramsay. A traversal-based
algorithm for higher-order model checking. In
*Proc. of ICFP 2012*, pp. 353-364. ACM, 2012. [doi link] - L. Ong, S. J. Ramsay. Verifying higher-order functional programs
with pattern-matching algebraic data types. In
*Proc. of POPL 2011*, pp. 587-598. ACM 2011. [doi link]

Last changed **
April 17, 2016 21:11 EET**
by
local organizers, ewscs13(at)cs.ioc.ee

EWSCS'13 page:
http://cs.ioc.ee/ewscs/2013/