A type-directed abstraction refinement approach to higher-order model checking

Steven J Ramsay, Robin P Neatherway, C-H Luke Ong

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

32 Citations (Scopus)
279 Downloads (Pure)

Abstract

The trivial-automaton model checking problem for higher-order recursion schemes has become a widely studied object in connection with the automatic verification of higher-order programs. The problem is formidably hard: despite considerable progress in recent years, no decision procedures have been demonstrated to scale robustly beyond recursion schemes that comprise more than a few hundred rewrite rules. We present a new, fixed-parameter polynomial time algorithm, based on a novel, type directed form of abstraction refinement in which behaviours of a scheme are distinguished by the abstraction according to the intersection types that they inhabit (the properties that they satisfy). Unlike other intersection type approaches, our algorithm reasons both about acceptance by the property automaton and acceptance by its dual, simultaneously, in order to minimize the amount of work done by converging on the solution to a problem instance from both sides. We have constructed Preface, a prototype implementation of the algorithm, and assembled an extensive body of evidence to demonstrate empirically that the algorithm readily scales to recursion schemes of several thousand rules, well beyond the capabilities of current state-of-the-art higher-order model checkers.
Original languageEnglish
Title of host publicationPOPL '2014 Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
PublisherAssociation for Computing Machinery (ACM)
Pages61-72
Number of pages12
ISBN (Print)9781450325448
DOIs
Publication statusPublished - 11 Jan 2014

Keywords

  • higher-order model checking
  • intersection types
  • abstraction refinement

Fingerprint Dive into the research topics of 'A type-directed abstraction refinement approach to higher-order model checking'. Together they form a unique fingerprint.

Cite this