skip to main content
10.1145/2364527.2364578acmconferencesArticle/Chapter ViewAbstractPublication PagesicfpConference Proceedingsconference-collections
research-article

A traversal-based algorithm for higher-order model checking

Published: 09 September 2012 Publication History

Abstract

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.

References

[1]
Klaus Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Comp. Sci., 3(3), 2007.
[2]
Thomas Ball, Rupak Majumdar, Todd D. Millstein, and Sriram K. Rajamani. Automatic predicate abstraction of C programs. In PLDI, pages 203--213, 2001.
[3]
Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. The software model checker blast. STTT, 9(5-6):505--525, 2007.
[4]
Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible pushdown automata and recursion schemes. In LICS, pages 452--461, 2008.
[5]
J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. Inf. Comput., 163(2):285--408, 2000.
[6]
Teodor Knapik, Damian Niwinski, and Pawel Urzyczyn. Higher-order pushdown trees are easy. In FoSSaCS, pages 205--222, 2002.
[7]
Naoki Kobayashi. Model-checking higher-order functions. In PPDP, pages 25--36, 2009.
[8]
Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In POPL, pages 416--428, 2009.
[9]
Naoki Kobayashi. http://www-kb.is.s.u-tokyo.ac.jp/~koba/trecs/. 2009.
[10]
Naoki Kobayashi. A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes. In FOSSACS, pages 260--274, 2011.
[11]
Naoki Kobayashi and C.-H. Luke Ong. Complexity of model checking recursion schemes for fragments of the modal mu-calculus. In ICALP (2), pages 223--234, 2009.
[12]
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.
[13]
Naoki Kobayashi, Naoshi Tabuchi, and Hiroshi Unno. Higher-order multi-parameter tree transducers and recursion schemes for program verification. In POPL, pages 495--508, 2010.
[14]
Neil Mitchell and Colin Runciman. Not all patterns, but enough - an automatic verifier for partial but sufficient pattern matching. In Haskell '08: Proceedings of the first ACM SIGPLAN symposium on Haskell, pages 49--60. ACM, September 2008.
[15]
Robin P. Neatherway, C.-H. Luke Ong, and Steven J. Ramsay. A traversal-based algorithm for higher-order model checking. Long version, available from: http://mjolnir.cs.ox.ac.uk/papers/traversal.pdf, 2012.
[16]
C.-H. Luke Ong. On model-checking trees generated by higherorder recursion schemes. In LICS, pages 81--90, 2006. Long version (55 pp.) http://www.cs.ox.ac.uk/people/luke.ong/personal/publications/ntree.pdf.
[17]
C.-H. Luke Ong and Steven J. Ramsay. Verifying functional programs with pattern matching algebraic data types. In POPL, pages 587--598, 2011.
[18]
Jakob Rehof and Torben Æ. Mogensen. Tractable constraints in finite semilattices. Sci. Comput. Program., 35(2):191--221, 1999.
[19]
Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. In ICALP (2), pages 162--173, 2011.

Cited By

View all
  • (2025)Space-Efficient Model-Checking of Higher-Order Recursion SchemesVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-82700-6_2(29-51)Online publication date: 20-Jan-2025
  • (2021)Modelling and verification of parameterized architectures: A functional approachIET Computers & Digital Techniques10.1049/cdt2.1202415:5(335-348)Online publication date: 22-Mar-2021
  • (2019)10 Years of the Higher-Order Model Checking Project (Extended Abstract)Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming10.1145/3354166.3354167(1-2)Online publication date: 7-Oct-2019
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programming
September 2012
392 pages
ISBN:9781450310543
DOI:10.1145/2364527
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 47, Issue 9
    ICFP '12
    September 2012
    368 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2398856
    Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 September 2012

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. higher-order programs
  2. model-checking

Qualifiers

  • Research-article

Conference

ICFP'12
Sponsor:

Acceptance Rates

ICFP '12 Paper Acceptance Rate 32 of 88 submissions, 36%;
Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25
ACM SIGPLAN International Conference on Functional Programming
October 12 - 18, 2025
Singapore , Singapore

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)4
  • Downloads (Last 6 weeks)1
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2025)Space-Efficient Model-Checking of Higher-Order Recursion SchemesVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-82700-6_2(29-51)Online publication date: 20-Jan-2025
  • (2021)Modelling and verification of parameterized architectures: A functional approachIET Computers & Digital Techniques10.1049/cdt2.1202415:5(335-348)Online publication date: 22-Mar-2021
  • (2019)10 Years of the Higher-Order Model Checking Project (Extended Abstract)Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming10.1145/3354166.3354167(1-2)Online publication date: 7-Oct-2019
  • (2018)Lazy Abstraction for Higher-Order Program VerificationProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236969(1-13)Online publication date: 3-Sep-2018
  • (2018)Constrained Dynamic Tree NetworksReachability Problems10.1007/978-3-030-00250-3_4(45-58)Online publication date: 30-Aug-2018
  • (2017)A cartesian-closed category for higher-order model checkingProceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3329995.3330055(1-12)Online publication date: 20-Jun-2017
  • (2017)Soft contract verification for higher-order stateful programsProceedings of the ACM on Programming Languages10.1145/31581392:POPL(1-30)Online publication date: 27-Dec-2017
  • (2017)Linearity in higher-order recursion schemesProceedings of the ACM on Programming Languages10.1145/31581272:POPL(1-29)Online publication date: 27-Dec-2017
  • (2017)The 2017 Alonzo Church awardACM SIGLOG News10.1145/3129173.31291744:3(3-9)Online publication date: 28-Jul-2017
  • (2017)On the relationship between higher-order recursion schemes and higher-order fixpoint logicACM SIGPLAN Notices10.1145/3093333.300985452:1(246-259)Online publication date: 1-Jan-2017
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media