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

TLDR

Type‑based model‑checking algorithms for higher‑order recursion schemes are a promising approach to verifying functional programs, and pattern‑matching recursion schemes extend these schemes by incorporating pattern‑matching in the defining rules. This paper introduces pattern‑matching recursion schemes as an accurate model of computation for functional programs manipulating algebraic data‑types and addresses the undecidable verification problem of whether all terms reachable from a regular input set satisfy a given correctness property. The authors solve the verification problem with a sound semi‑algorithm based on model‑checking and counterexample‑guided abstraction refinement that constructs an order‑n weak PMRS over‑approximating first‑order pattern‑matching while preserving higher‑order control flow, refining the abstraction by unfolding pattern‑matching rules when spurious violations occur. The method guarantees termination on no‑instances and shows that model‑checking weak PMRS is decidable via a variation of Kobayashi's type‑based approach.

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.