research-article

Verifying higher-order functional programs with pattern-matching algebraic data types

Authors:

C.-H. Luke Ong,

Steven J. RamsayAuthors Info & Claims

POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 587 - 598

https://doi.org/10.1145/1926385.1926453

Published: 26 January 2011 Publication History

Abstract

Type-based model checking algorithms for higher-order recursion schemes have recently emerged as a promising approach to the verification of functional programs. We introduce pattern-matching recursion schemes (PMRS) as an accurate model of computation for functional programs that manipulate algebraic data-types. PMRS are a natural extension of higher-order recursion schemes that incorporate pattern-matching in the defining rules.

This paper is concerned with the following (undecidable) verification problem: given a correctness property φ, a functional program ℘ (qua PMRS) and a regular input set ℑ, does every term that is reachable from ℑ under rewriting by ℘ satisfy φ? To solve the PMRS verification problem, we present a sound semi-algorithm which is based on model-checking and counterexample guided abstraction refinement. Given a no-instance of the verification problem, the method is guaranteed to terminate.

From an order-n PMRS and an input set generated by a regular tree grammar, our method constructs an order-n weak PMRS which over-approximates only the first-order pattern-matching behaviour, whilst remaining completely faithful to the higher-order control flow. Using a variation of Kobayashi's type-based approach, we show that the (trivial automaton) model-checking problem for weak PMRS is decidable. When a violation of the property is detected in the abstraction which does not correspond to a violation in the model, the abstraction is automatically refined by `unfolding' the pattern-matching rules in the program to give successively more and more accurate weak PMRS models.

Supplementary Material

MP4 File (53-mpeg-4.mp4)

Download
457.23 MB

References

[1]

W. Blum and C.-H. L. Ong. Path-correspondence theorems and their applications. Preprint, 2009.

[2]

E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV '00: Proceedings of the 12th International Conference on Computer Aided Verification, pages 154--169, London, UK, 2000. Springer-Verlag.

Digital Library

[3]

A. Igarashi and N. Kobayashi. Resource usage analysis. ACM Trans. Program. Lang. Syst., 27(2):264--313, 2005.

Digital Library

[4]

N. D. Jones. Flow analysis of lambda expressions (preliminary version). In Proceedings of the 8th Colloquium on Automata, Languages and Programming, pages 114--128. Springer-Verlag, 1981. ISBN 3-540-10843-2.

Digital Library

[5]

N. D. Jones and N. Andersen. Flow analysis of lazy higher-order functional programs. Theoretical Computer Science, 375:120--136, 2007.

Digital Library

[6]

N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In Proceedings of POPL 2009, pages 416--428. ACM Press, 2009.

Digital Library

[7]

N. Kobayashi. Model-checking higher-order functions. In PPDP, pages 25--36, 2009.

Digital Library

[8]

N. Kobayashi and C.-H. L. Ong. A type theory equivalent to the modal mu-calculus model checking ofhigher-order recursion schemes. In Proceedings of LICS 2009. IEEE Computer Society, 2009.

Digital Library

[9]

N. Kobayashi, N. Tabuchi, and H. Unno. Higher-order multi-parameter tree transducers and recursion schemes for program veri- fication. In POPL, pages 495--508, 2010.

Digital Library

[10]

J. Kochems. Approximating reachable terms of functional programs. University of Oxford MMathsCompSc thesis, 2010.

[11]

R. P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton University Press, 1994.

Digital Library

[12]

J. Midtgaard. Control-flow analysis of functional programs. Technical Report BRICS RS-07-18, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, Dec 2007. URL http://www.brics.dk/RS/07/18/BRICS-RS-07-18.pdf.

[13]

F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag New York, 1999.

Digital Library

[14]

C.-H. L. Ong. On model-checking trees generated by higher-order recursion schemes. In Proceedings 21st Annual IEEE Symposium on Logic in Computer Science, Seattle, pages 81--90. Computer Society Press, 2006. Long version (55 pp.) downloadable at users.comlab.ox.ac.uk/luke.ong/.

Digital Library

[15]

C.-H. L. Ong and S. J. Ramsay. Verifying higher-order functional programs with pattern-matching al- gebraic data types. Long version, available from: https://mjolnir.comlab.ox.ac.uk/papers/pmrs.pdf.

Digital Library

[16]

C.-H. L. Ong and N. Tzevelekos. Functional reachability. In LICS, pages 286--295, 2009.

Digital Library

[17]

O. Shivers. Control-flow analysis of higher-order languages. PhD thesis, Carnegie-Mellon University, 1991.

Digital Library

Cited By

Kobayashi N(2025)On Decidable and Undecidable Extensions of Simply Typed Lambda CalculusProceedings of the ACM on Programming Languages10.1145/37048759:POPL(1136-1166)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704875
Sekiyama TUnno H(2024)Higher-Order Model Checking of Effect-Handling Programs with Answer-Type ModificationProceedings of the ACM on Programming Languages10.1145/36898058:OOPSLA2(2662-2691)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689805
Bautista SJensen TMontagu B(2024)An input–output relational domain for algebraic data types and functional arraysFormal Methods in System Design10.1007/s10703-024-00456-zOnline publication date: 13-Jun-2024
https://doi.org/10.1007/s10703-024-00456-z
Show More Cited By

Index Terms

Verifying higher-order functional programs with pattern-matching algebraic data types

Recommendations

Verifying higher-order functional programs with pattern-matching algebraic data types
POPL '11

Type-based model checking algorithms for higher-order recursion schemes have recently emerged as a promising approach to the verification of functional programs. We introduce pattern-matching recursion schemes (PMRS) as an accurate model of computation ...
Types and higher-order recursion schemes for verification of higher-order programs
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We propose a new verification method for temporal properties of higher-order functional programs, which takes advantage of Ong's recent result on the decidability of the model-checking problem for higher-order recursion schemes (HORS's). A program is ...
Types and higher-order recursion schemes for verification of higher-order programs
POPL '09

We propose a new verification method for temporal properties of higher-order functional programs, which takes advantage of Ong's recent result on the decidability of the model-checking problem for higher-order recursion schemes (HORS's). A program is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2011

652 pages

ISBN:9781450304900

DOI:10.1145/1926385

General Chair:
Thomas Ball
Microsoft Research, USA
,
Program Chair:
Mooly Sagiv
Tel Aviv University, Israel

ACM SIGPLAN Notices Volume 46, Issue 1
POPL '11
January 2011
624 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1925844
Issue’s Table of Contents

Copyright © 2011 ACM.

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

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 January 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '11

Sponsor:

SIGPLAN

POPL '11: The 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 26 - 28, 2011

Texas, Austin, USA

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

97
Total Citations
View Citations
553
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)2

Reflects downloads up to 12 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Kobayashi N(2025)On Decidable and Undecidable Extensions of Simply Typed Lambda CalculusProceedings of the ACM on Programming Languages10.1145/37048759:POPL(1136-1166)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704875
Sekiyama TUnno H(2024)Higher-Order Model Checking of Effect-Handling Programs with Answer-Type ModificationProceedings of the ACM on Programming Languages10.1145/36898058:OOPSLA2(2662-2691)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689805
Bautista SJensen TMontagu B(2024)An input–output relational domain for algebraic data types and functional arraysFormal Methods in System Design10.1007/s10703-024-00456-zOnline publication date: 13-Jun-2024
https://doi.org/10.1007/s10703-024-00456-z
Sato R(2023)Refinement Types for Call-by-name ProgramsJournal of Information Processing10.2197/ipsjjip.31.70831(708-721)Online publication date: 2023
https://doi.org/10.2197/ipsjjip.31.708
Kobayashi NTanahashi KSato RTsukada T(2023)HFL(Z) Validity Checking for Automated Program VerificationProceedings of the ACM on Programming Languages10.1145/35711997:POPL(154-184)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571199
Farzan ANicolet V(2023)Partial bounding for recursive function synthesisFormal Methods in System Design10.1007/s10703-023-00417-y63:1-3(172-205)Online publication date: 16-May-2023
https://doi.org/10.1007/s10703-023-00417-y
Farzan ALette DNicolet VJhala RDillig I(2022)Recursion synthesis with unrealizability witnessesProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523726(244-259)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523726
Bautista SJensen TMontagu B(2022)Lifting Numeric Relational Domains to Algebraic Data TypesStatic Analysis10.1007/978-3-031-22308-2_6(104-134)Online publication date: 2-Dec-2022
https://doi.org/10.1007/978-3-031-22308-2_6
Cirstea HLermusiaux PMoreau P(2021)Static analysis of pattern-free propertiesProceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming10.1145/3479394.3479404(1-13)Online publication date: 6-Sep-2021
https://dl.acm.org/doi/10.1145/3479394.3479404
Jones ERamsay S(2021)Intensional datatype refinement: with application to scalable verification of pattern-match safetyProceedings of the ACM on Programming Languages10.1145/34343365:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434336
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten