Higher-Order Model Checking
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.
- 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]
April 17, 2016 21:11 EET
local organizers, ewscs13(at)cs.ioc.ee
EWSCS'13 page: http://cs.ioc.ee/ewscs/2013/