# Higher-Order Model Checking

**NII Shonan Meeting: **

**@ Shonan Village Center****, March 14-17, 2016**

## Organizers

- Naoki Kobayashi, The University of Tokyo, Japan
- Luke Ong, University of Oxford, UK
- Igor Walukiewicz, CNRS, LaBRI, Bordeaux University, France

## Overview

**Description of the meeting**

Finite state model checking has been widely studied and successfully applied to system verification. The main theme of this meeting, *higher-order model checking*, is a generalization of finite state model checking, obtained by replacing finite state models with more expressive models called recursion schemes. Higher-order model checking has found applications in analysis of object-oriented and concurrent programs with recursion and higher-order procedures.

Recursion schemes are a kind of simply-typed grammar for generating possibly infinite ranked trees. A recursion scheme is a finite system of equations, defining a finite set of higher-order functions by mutual recursion. The order of a recursion scheme is given by the highest type-theoretic order of the functions defined by it. From a programming language perspective, recursion schemes may be viewed as programs (i.e. closed, ground-type terms) of the simply-typed lambda calculus with recursion, constructed from a set of uninterpreted function symbols. Higher-order model checking is the model checking of trees generated by recursion schemes. The higher-order model checking problem asks, given a recursion scheme G and a correctness property φ, whether the tree generated by G satisfies φ.

The early work in the 1970s on (tree-generating) higher-order recursion schemes was mostly about questions of expressivity. The decision problem was first posed in the present form by Knapik et al. [5, 6]. They considered recursion schemes subject to a syntactic constraint called *safety*. Their main result is that, when restricted to trees generated by safe recursion schemes, the higher-order model checking problem with respect to monadic second- order (MSO) properties is decidable. However the general MSO higher-order model checking problem was left open. In [12], Ong proved that the modal mu-calculus model checking problem of trees generated by arbitrary order-*n* recursion schemes is *n*-EXPTIME complete. Since MSO logic and the modal mu-calculus are equi-expressive over trees, the MSO higher-order model checking problem is decidable.

The last fifteen years or so have seen a growth of interest in higher-order model checking from both the theory and practice communities. Since the MSO decidability result [12], which was proved using insights from game semantics [4], a variety of semantic and algorithmic techniques and models of computation have been employed to design higher-order model checking algorithms, notably, intersection types [7, 11], collapsible pushdown automata [3] and Krivine machines [15]. Algorithmic properties that refine and extend the decidability of MSO local model checking have also been introduced, such as logical reflection [1], effective selection [2] and transfer theorem [16]. One recent trend, initiated by Salvati and Walukiewicz, is the development of effective denotational semantics for an approach to higher-order model checking by evaluation [18, 17, 21].

Recursion schemes are a very expressive family of generators of trees: the trees that are generated at orders 0, 1 and 2 are respectively the regular trees, algebraic trees (i.e. those generated by context-free tree grammars) and hyperalgebraic trees. There have been advances in the understanding of the relationship between higher-order families of generators. Hague et al. [3] showed that order-*n* recursion schemes generate the same class of trees as order-*n* collapsible pushdown automata. More recently, Parys [13] proved the Safety Conjecture, thus confirming the intuition that the safety constraint restricts the expressive power of recursion schemes, or equivalently that order-*n* collapsibile pushdown automata are more expressive than order-*n* pushdown automata.

Recursion schemes are thus an appealing abstract model for model checking higher-order programs: not only are they highly expressive, the trees they generate also enjoy a rich and decidable logical theory. In [7, 8], Kobayashi introduced an approach to the verification of safety properties of functional programs by reduction to higher-order model checking. His verification method is sound, complete, and automatic for a range of verification problems such as reachability, flow analysis, and resource usage for simply-typed recursive functional programs generated from finite base types. Although the worst-case complexity of higher-order model checking is hyper-exponential, there have been remarkable advances in the design of model checking algorithms. The time complexity of state-of-the-art model checking algorithms, PREFACE [14] and HORSATZDD [19], are fixed-parameter polynomial in the size of the recursion schemes, and scale readily to many thousands of rules. In addition to the model checking of object-oriented [9] and concurrent programs [22], higher-order model checking have found applications in program analysis [20], and data compression [10].

**Topics**

*Extensions of HOMC*: beyond simple types (e.g. untyped and recursively typed recursion schemes, higher-type Böhm trees); beyond omega-regular properties: finitary parity, omega-B, stack unboundedness, etc.

*“Practical” HOMC algorithms*. E.g. HORSATZDD, Preface, C-SHORe, etc.

*Applications of HOMC*: program verification (functional, object-orientation, concurrency), program analysis, data compression, security, etc.

*Higher-order grammars and pushdown automata*. Context sensitivity of unsafe Maslov languages and other open problems.*Effective denotational semantics and strategy-aware models for HOMC*. Compositional approaches to HOMC.

**Format of the Meeting**?????????? We plan to organize some of the following activities:

- Survey and tutorial lectures
- Technical presentations
- Panel / thematic discussions
- Open problems session
- Demos of software tools

**References**

[1] Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, and Olivier Serre. Recursion Schemes and Logical Reflection. In *LICS*, pages 120?129, 2010.

[2] Arnaud Carayol and Olivier Serre. Collapsible Pushdown Automata and Labeled Recursion Schemes: Equivalence, Safety and Effective Selection. In *LICS*, pages 165?174, 2012.

[3] Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible Pushdown Automata and Recursion Schemes. In *LICS*, pages 452?461, 2008.

[4] J. M. E. Hyland and C.-H. Luke Ong. On Full Abstraction for PCF: I, II and III.

*Information and Computation*, 163(2):285?408, 2000.

[5] Teodor Knapik, Damian Niwiński, and Pawel Urzyczyn. Deciding monadic theories of hyperalgebraic trees. *TLCA*, pages 253?267, 2001.

[6] Teodor Knapik, Damian Niwiński, and Pawel Urzyczyn. Higher-order pushdown trees are easy. In *FoSSaCS*, pages 205?222, 2002.

[7] Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher- order programs. In *POPL*, page 416, January 2009.

[8] Naoki Kobayashi. Model Checking Higher-Order Programs. *JACM*, 60(3), 2013.

[9] Naoki Kobayashi and Atsushi Igarashi. Model-Checking Higher-Order Programs with Recursive Types. In *ESOP*, pages 431?450, 2013.

[10] Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, and Kazuya Yaguchi. Functional programs as compressed data. *Higher-Order and Symbolic Computation*, (2012):1? 46, 2013.

[11] Naoki Kobayashi and C.-H. Luke Ong. A Type System Equivalent to the Modal Mu- Calculus Model Checking of Higher-Order Recursion Schemes. In *LICS*, pages 179?188, 2009.

[12] C.-H. Luke Ong. On Model Checking Trees Generated by Higher-Order Recursion Schemes. In *LICS*, pages 81?90, 2006.

[13] Pawe Parys. On the Significance of the Collapse Operation. In *LICS*, pages 521?530.

IEEE, June 2012.

[14] Steven J. Ramsay, Robin P. Neatherway, and C.-H. Luke Ong. An Abstraction Refinement Approach to Higher-Order Model Checking. In *POPL*, pages 61?72, New York, USA, 2014. ACM Press.

[15] Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. In *ICALP*, pages 162?173, 2011.

[16] Sylvain Salvati and Igor Walukiewicz. Evaluation is MSOL-compatible. In *FSTTCS*, pages 103?114, 2013.

[17] Sylvain Salvati and Igor Walukiewicz. Using Models to Model-Check Recursive Schemes.

In *TLCA*, pages 189?204, 2013.

[18] Sylvain Salvati and Igor Walukiewicz. Typing Weak MSOL Properties. In *FoSSaCS*, volume 7794, pages 129?144, 2015.

[19] Taku Terao and Naoki Kobayashi. A ZDD-Based Efficient Higher-Order Model.?? In *APLAS*, pages 354?371, 2014.

[20] Yoshihiro Tobita, Takeshi Tsukada, and Naoki Kobayashi. Exact flow analysis by higher- order model checking. *FLOPS*, pages 275?289, 2012.

[21] Takeshi Tsukada and C.-H. Luke Ong. Compositional Higher-order Model Checking via omega-Regular Games over Boehm trees. In *CSL-LICS*, 2014.

[22] Kazuhide Yasukata, Naoki Kobayashi, and Kazutaka Matsuda. Pairwise Reachability Analysis for Higher Order Concurrent Programs by Higher-Order Model. In *CONCUR*, pages 312?326, 2014.