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

Luke Ong, Steven Ramsay

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

41 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationPOPL '11 Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
PublisherAssociation for Computing Machinery (ACM)
Pages587-598
Number of pages12
ISBN (Print)978-1-4503-0490-0
DOIs
Publication statusPublished - Jan 2011

Fingerprint

Dive into the research topics of 'Verifying higher-order functional programs with pattern matching algebraic data types'. Together they form a unique fingerprint.

Cite this