Verifying Higher-Order Functional Programs with Pattern-Matching Algebraic Data Types
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 algebrai...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Published: |
2011
|
| _version_ | 1797102619275034624 |
|---|---|
| author | Ong, C Ramsay, S ACM |
| author_facet | Ong, C Ramsay, S ACM |
| author_sort | Ong, C |
| collection | OXFORD |
| description | 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 P (qua PMRS) and a regular input set I, does every term that is reachable from I under rewriting by P satisfy φ? To solve the PMRS verification problem, we present a sound semi-algorithm which is based on model-checking and counterexample guided abstraction finement. 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. Copyright © 2011 ACM. |
| first_indexed | 2024-03-07T06:08:30Z |
| format | Conference item |
| id | oxford-uuid:eea8c42f-a377-4de7-881b-d78f8f91fb24 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:08:30Z |
| publishDate | 2011 |
| record_format | dspace |
| spelling | oxford-uuid:eea8c42f-a377-4de7-881b-d78f8f91fb242022-03-27T11:34:26ZVerifying Higher-Order Functional Programs with Pattern-Matching Algebraic Data TypesConference itemhttp://purl.org/coar/resource_type/c_5794uuid:eea8c42f-a377-4de7-881b-d78f8f91fb24Symplectic Elements at Oxford2011Ong, CRamsay, SACMType-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 P (qua PMRS) and a regular input set I, does every term that is reachable from I under rewriting by P satisfy φ? To solve the PMRS verification problem, we present a sound semi-algorithm which is based on model-checking and counterexample guided abstraction finement. 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. Copyright © 2011 ACM. |
| spellingShingle | Ong, C Ramsay, S ACM Verifying Higher-Order Functional Programs with Pattern-Matching Algebraic Data Types |
| title | Verifying Higher-Order Functional Programs with Pattern-Matching Algebraic Data Types |
| title_full | Verifying Higher-Order Functional Programs with Pattern-Matching Algebraic Data Types |
| title_fullStr | Verifying Higher-Order Functional Programs with Pattern-Matching Algebraic Data Types |
| title_full_unstemmed | Verifying Higher-Order Functional Programs with Pattern-Matching Algebraic Data Types |
| title_short | Verifying Higher-Order Functional Programs with Pattern-Matching Algebraic Data Types |
| title_sort | verifying higher order functional programs with pattern matching algebraic data types |
| work_keys_str_mv | AT ongc verifyinghigherorderfunctionalprogramswithpatternmatchingalgebraicdatatypes AT ramsays verifyinghigherorderfunctionalprogramswithpatternmatchingalgebraicdatatypes AT acm verifyinghigherorderfunctionalprogramswithpatternmatchingalgebraicdatatypes |