A traversal-based algorithm for higher-order model checking

Robin Neatherway, Luke Ong, Steven Ramsay

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

13 Citations (Scopus)
11 Downloads (Pure)


Higher-order model checking - the model checking of trees generated by higher-order recursion schemes (HORS) - is a natural generalisation of finite-state and pushdown model checking. Recent work has shown that it can serve as a basis for software model checking for functional languages such as ML and Haskell. In this paper, we introduce higher-order recursion schemes with cases (HORSC), which extend HORS with a definition-by-cases construct (to express program branching based on data) and non-determinism (to express abstractions of behaviours). This paper is a study of the universal HORSC model checking problem for deterministic trivial automata: does the automaton accept every tree in the tree language generated by the given HORSC? We first characterise the model checking problem by an intersection type system extended with a carefully restricted form of union types. We then present an algorithm for deciding the model checking problem, which is based on the notion of traversals induced by the fully abstract game semantics of these schemes, but presented as a goal-directed construction of derivations in the intersection and union type system. We view HORSC model checking as a suitable backend engine for an approach to verifying functional programs. We have implemented the algorithm in a tool called TravMC, and demonstrated its effectiveness on a test suite of programs, including abstract models of functional programs obtained via an abstraction-refinement procedure from pattern-matching recursion schemes.
Original languageEnglish
Title of host publicationICFP '12 Proceedings of the 17th Annual ACM SIGPLAN International Conference on Functional Programming
PublisherAssociation for Computing Machinery (ACM)
Number of pages12
ISBN (Print)978-1-4503-1054-3
Publication statusPublished - Sept 2012


Dive into the research topics of 'A traversal-based algorithm for higher-order model checking'. Together they form a unique fingerprint.

Cite this