C.-H. Luke Ong
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.
Supplemental Material
- W. Blum and C.-H. L. Ong. Path-correspondence theorems and their applications. Preprint, 2009.Google Scholar
- 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. Google ScholarDigital Library
- A. Igarashi and N. Kobayashi. Resource usage analysis. ACM Trans. Program. Lang. Syst., 27(2):264--313, 2005. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- N. D. Jones and N. Andersen. Flow analysis of lazy higher-order functional programs. Theoretical Computer Science, 375:120--136, 2007. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- N. Kobayashi. Model-checking higher-order functions. In PPDP, pages 25--36, 2009. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- J. Kochems. Approximating reachable terms of functional programs. University of Oxford MMathsCompSc thesis, 2010.Google Scholar
- R. P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton University Press, 1994. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag New York, 1999. Google ScholarDigital Library
- 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/. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- C.-H. L. Ong and N. Tzevelekos. Functional reachability. In LICS, pages 286--295, 2009. Google ScholarDigital Library
- O. Shivers. Control-flow analysis of higher-order languages. PhD thesis, Carnegie-Mellon University, 1991. Google ScholarDigital Library
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 '11Type-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 languagesWe 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 '09We 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