Model Checking Higher-Order Programs

Abstract

We propose a novel verification method for higher-order functional programs based on higher-order model checking, or more precisely, model checking of higher-order recursion schemes (recursion schemes, for short). The most distinguishing feature of our verification method for higher-order programs is that it is sound, complete, and automatic for the simply typed λ-calculus with recursion and finite base types, and for various program verification problems such as reachability, flow analysis, and resource usage verification. We first show that a variety of program verification problems can be reduced to model checking problems for recursion schemes, by transforming a program into a recursion scheme that generates a tree representing all the interesting possible event sequences of the program. We then develop a new type-based model-checking algorithm for recursion schemes and implement a prototype recursion scheme model checker. To our knowledge, this is the first implementation of a recursion scheme model checker. Experiments show that our model checker is reasonably fast, despite the worst-case time complexity of recursion scheme model checking being hyperexponential in general. Altogether, the results provide a new, promising approach to verification of higher-order functional programs.

References

1. Objective caml. http://caml.inria.fr/ocaml/.
2. Aehlig, K. 2007. A finite semantics of simply-typed lambda terms for infinite runs of automata. Log. Meth. Comput. Sci. 3, 3.
3. Aehlig, K., de Miranda, J. G., and Ong, C.-H. L. 2005. The monadic second order theory of trees given by arbitrary level-two recursion schemes is decidable. In Proceedings of TLCA 2005. Lecture Notes in Computer Science, vol. 3461, Springer, 39--54.
4. Appel, A. W. 1992. Compiling with Continuations. Cambridge University Press.
5. Bakewell, A. and Ghica, D. R. 2008. On-the-fly techniques for game-based software model checking. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008). Lecture Notes in Computer Science, vol. 4963, Springer, 78--92.
6. Ball, T. and Rajamani, S. K. 2002. The SLAM project: Debugging system software via static analysis. In Proceedings of the ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 1--3.
7. Ball, T., Majumdar, R., Millstein, T. D., and Rajamani, S. K. 2001. Automatic predicate abstraction of C programs. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 203--213.
8. Barendregt, H., Coppo, M., and Dezani-Ciancaglini, M. 1983. A filter lambda model and the completeness of type assignment. J. Symb. Log. 48, 4, 931--940.
9. Beckmann, A. 2001. Exact bounds for lengths of reductions in typed lambda-calculus. J. Symb. Log. 66, 3, 1277--1285.
10. Benzaken, V., Castagna, G., and Frisch, A. 2003. CDuce: An XML-centric general-purpose language. In Proceedings of ICFP 2003. ACM, 51--63.
11. Beyer, D., Henzinger, T. A., Jhala, R., and Majumdar, R. 2007. The software model checker Blast. Int. J. Soft. Tools Tech. Trans. 9, 5--6, 505--525.
12. Blume, M., Acar, U. A., and Chae, W. 2008. Exception handlers as extensible cases. In Proceedings of APLAS. Lecture Notes in Computer Science, vol. 5356, Springer, 273--289.
13. Boudol, G. 2008. On strong normalization and type inference in the intersection type discipline. Theoret. Comput. Sci. 398, 1--3, 63--81.
14. Burn, G. L., Hankin, C., and Abramsky, S. 1986. Strictness analysis for higher-order functions. Sci. Comput. Program. 7, 3, 249--278.
15. Cachat, T. and Walukiewicz, I. 2007. The complexity of games on higher order pushdown automata. CoRR abs/0705.0262.
16. Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2003. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50, 5, 752--794.
17. Clarke, E. M., Grumberg, O., and Peled, D. A. 1999. Model Checking. The MIT Press.
18. Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., and Vardi, M. Y. 2007. Proving that programs eventually do something good. In Proceedings of the ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 265--276.
19. Coppo, M., Dezani-Ciancaglini, M., and Sallé, P. 1979. Functional characterization of some semantic equalities inside lambda-calculus. In Proceedings of ICALP’79. Lecture Notes in Computer Science, vol. 71, Springer, 133--146.
20. Coppo, M., Dezani-Ciancaglini, M., and Venneri, B. 1980. Principal type schemes and lambda-calculus semantics. In Proceedings of the Essays on Combinatory Logic, Lambda Calculus, and Foundation, Academic Press, 535--560.
21. Coppo, M., Dezani-Ciancaglini, M., and Venneri, B. 1981. Functional characters of solvable terms. Math. Logic Quart. 27, 2--6, 45--58.
22. Courcelle, B. 1983. Fundamental properties of infinite trees. Theoret. Comput. Sci. 25, 95--169.
23. Damas, L. and Milner, R. 1982. Principal type-schemes for functional programs. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL). ACM Press, 207--212.
24. Damas, L. M. M. 1984. Type assignment in programming languages. Ph.D. dissertation. University of Edinburgh.
25. Damm, W. 1982. The IO- and OI-hierarchies. Theoret. Comput. Sci. 20, 95--207.
26. Danvy, O. and Filinski, A. 1992. Representing control: A study of the cps transformation. Math. Struct. Comput. Sci. 2, 4, 361--391.
27. DeLine, R. and Fähndrich, M. 2001. Enforcing high-level protocols in low-level software. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 59--69.
28. Dillig, I., Dillig, T., and Aiken, A. 2008. Sound, complete and scalable path-sensitive analysis. In Proceedings of PLDI’08. ACM, 270--280.
29. Emerson, E. A. and Jutla, C. S. 1991. Tree automata, mu-calculus and determinacy (extended abstract). In Proceedings of the 32nd Annual Symposium on Foundations of Computer Science (FOCS’91). IEEE Computer Society Press, 368--377.
30. Foster, J. S., Terauchi, T., and Aiken, A. 2002. Flow-sensitive type qualifiers. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 1--12.
31. Freeman, T. and Pfenning, F. 1991. Refinement types for ML. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 268--277.
32. Frisch, A. and Hosoya, H. 2007. Towards practical typechecking for macro tree transducers. In Proceedings of the 11th International Symposium on Database Programming Languages (DBPL’07). Lecture Notes in Computer Science, vol. 4797, Springer, 246--260.
33. Graf, S. and Saïdi, H. 1997. Construction of abstract state graphs with PVS. In Proceedings of CAV’97. Lecture Notes in Computer Science, vol. 1254, Springer, 72--83.
34. Hague, M., Murawski, A., Ong, C.-H. L., and Serre, O. 2008. Collapsible pushdown automata and recursion schemes. In Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 452--461.
35. Henglein, F. and Mairson, H. G. 1994. The complexity of type inference for higher-order typed lambda calculi. J. Funct. Prog. 4, 4, 435--477.
36. Henglein, F. and Mossin, C. 1994. Polymorphic binding-time analysis. In Proceedings of the 5th European Symposium on Programming (ESOP’94). Lecture Notes in Computer Science, vol. 788, Springer, 287--301.
37. Henzinger, T. A., Jhala, R., Majumdar, R., and Sutre, G. 2002. Lazy abstraction. In Proceedings of the ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 58--70.
38. Hosoya, H., Vouillon, J., and Pierce, B. C. 2005. Regular expression types for XML. ACM Trans. Program. Lang. Syst. 27, 1, 46--90.
39. Igarashi, A. and Kobayashi, N. 2005. Resource usage analysis. ACM Trans. Prog. Lang. Syst. 27, 2, 264--313.
40. Iwama, F., Igarashi, A., and Kobayashi, N. 2006. Resource usage analysis for a functional language with exceptions. In Proceedings of the ACM SIGPLAN’06 Workshop on Partial Evaluation and Program Manipulation (PEPM’06). ACM, 38--47.
41. Jensen, T. P. 1991. Strictness analysis in logical form. In Proceedings of the Functional Programming Languages and Computer Architecture (FPCA’91). Lecture Notes in Computer Science, vol. 523, Springer, 352--366.
42. Jensen, T. P. 1992. Abstract interpretation in logical form. Ph.D. dissertation. Imperial College.
43. Johnsson, T. 1985. Lambda lifting: Treansforming programs to recursive equations. In Proceedings of FPCA’85. Lecture Notes in Computer Science, vol. 201, Springer, 190--203.
44. Kfoury, A. J. and Wells, J. B. 2004. Principality and type inference for intersection types using expansion variables. Theoret. Comput. Sci. 311, 1--3, 1--70.
45. Kfoury, A. J., Tiuryn, J., and Urzyczyn, P. 1990. ML typability is DEXTIME-complete. In Proceedings of CAAP’90. Lecture Notes in Computer Science, vol. 431, Springer, 206--220.
46. Knapik, T., Niwinski, D., and Urzyczyn, P. 2001. Deciding monadic theories of hyperalgebraic trees. In Proceedings of the TLCA’01. Lecture Notes in Computer Science, vol. 2044, Springer, 253--267.
47. Knapik, T., Niwinski, D., and Urzyczyn, P. 2002. Higher-order pushdown trees are easy. In Proceedings of the FoSSaCS’02. Lecture Notes in Computer Science, vol. 2303, Springer, 205--222.
48. Knapik, T., Niwinski, D., Urzyczyn, P., and Walukiewicz, I. 2005. Unsafe grammars and panic automata. In Proceedings of the ICALP’05. Lecture Notes in Computer Science, vol. 3580, Springer, 1450--1461.
49. Knaster, B. 1927. Un théorème sur les fonctions d’ensembles. Ann. Soc. Polon. Math. 6, 133--134.
50. Kobayashi, N. 2009a. Model-checking higher-order functions. In Proceedings of PPDP’09. ACM, 25--36.
51. Kobayashi, N. 2009b. Types and higher-order recursion schemes for verification of higher-order programs. In Proceedings of the ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 416--428.
52. Kobayashi, N. 2010. Balancedness of high-level word languages is undecidable. draft.
53. Kobayashi, N. 2011. A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes. In Proceedings of FoSSaCS’11. Lecture Notes in Computer Science, vol. 6604, Springer, 260--274.
54. Kobayashi, N. and Ong, C.-H. L. 2009. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In Proceedings of LICS’09. IEEE Computer Society Press, 179--188.
55. Kobayashi, N. and Ong, C.-H. L. 2011. Complexity of model checking recursion schemes for fragments of the modal mu-calculus. Logic. Meth. Comput. Sci. 7, 4.
56. Kobayashi, N., Sato, R., and Unno, H. 2011. Predicate abstraction and CEGAR for higher-order model checking. In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 222--233.
57. Kobayashi, N., Tabuchi, N., and Unno, H. 2010. Higher-order multi-parameter tree transducers and recursion schemes for program verification. In Proceedings of the ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 495--508.
58. Kupferman, O., Vardi, M. Y., and Wolper, P. 2000. An automata-theoretic approach to branching-time model checking. J. ACM 47, 2, 312--360.
59. Leroy, X. and Pessaux, F. 2000. Type-based analysis of uncaught exceptions. ACM Trans. Prog. Lang. Syst. 22, 2, 340--377.
60. Loader, R. 2001. Finitary PCF is not decidable. Theoret. Comput. Sci. 266, 1--2, 341--364.
61. Mairson, H. G. 1990. Deciding ML typability is complete for deterministic exponential time. In Proceedings of the POPL. ACM, 382--401.
62. Mairson, H. G. 1992. A simple proof of a theorem of statman. Theoret. Comput. Sci. 103, 2, 387--394.
63. McMillan, K. L. 2006. Lazy abstraction with interpolants. In Proceedings of CAV’06. Lecture Notes in Computer Science, vol. 4144, Springer, 123--136.
64. Meyer, A. R. and Wand, M. 1985. Continuation semantics in typed lambda-calculi (summary). In Proceedings of the Logic of Programs. Lecture Notes in Computer Science, vol. 193, Springer, 219--224.
65. Might, M. and Shivers, O. 2008. Exploiting reachability and cardinality in higher-order flow analysis. J. Funct. Prog. 18, 5--6, 821--864.
66. Mossin, C. 2003. Exact flow analysis. Math. Struct. Comput. Sci. 13, 1, 125--156.
67. Mycroft, A. 1980. The theory and practice of transforming call-by-need into call-by-value. In Proceedings of the Symposium on Programming. Lecture Notes in Computer Science, vol. 83, Springer, 269--281.
68. Naik, M. 2003. A type system equivalent to a model checker. Master Thesis, Purdue University.
69. Naik, M. and Palsberg, J. 2005. A type system equivalent to a model checker. In Proceedings of the ESOP’05. Lecture Notes in Computer Science, vol. 3444, Springer, 374--388.
70. Nielson, F., Nielson, H. R., and Hankin, C. 1999. Principles of Program Analysis. Springer.
71. Ong, C.-H. L. 2006. On model-checking trees generated by higher-order recursion schemes. In Proceedings of the LICS’06. IEEE Computer Society Press, 81--90.
72. Ong, C.-H. L. and Ramsay, S. J. 2009. Subtyping for model checking recursion schemes. Preprint, July 6, 2009. (A summary appeared in Proceedings of the Oxford University Computing Laboratory Student Conference 2009, CS-RR-09-14).
73. Ong, C.-H. L. and Ramsay, S. 2011. Verifying higher-order programs with pattern-matching algebraic data types. In Proceedings of the ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 587--598.
74. Palsberg, J. 2001. Type-based analysis and applications. In Proceedings of PASTE’01. ACM, 20--27.
75. Plotkin, G. D. 1975. Call-by-name, call-by-value and the lambda-calculus. Theoret. Comput. Sci. 1, 2, 125--159.
76. Rehof, J. and Mogensen, T. 1999. Tractable constraints in finite semilattices. Sci. Comput. Progr. 35, 2, 191--221.
77. Ronchi Della Rocca, S. and Venneri, B. 1984. Principal type schemes for an extended type theory. Theoret. Comput. Sci. 28, 151--169.
78. Schwoon, S. 2002. Model-checking pushdown systems. Ph.D. dissertation, Technische Universität München.
79. Thomas, W. 1997. Languages, automata, and logic. In Handbook of Formal Languages vol. 3. Springer, 389--455.
80. Tobita, Y., Tsukada, T., and Kobayashi, N. 2012. Exact flow analysis by higher-order model checking. In Proceedings of FLOPS’12. Lecture Notes in Computer Science, vol. 7294, Springer, 275--289.
81. Tozawa, A. 2006. XML type checking using high-level tree transducer. In Proceedings of the 8th International Symposium on Functional and Logic Programming (FLOPS’06). Lecture Notes in Computer Science, vol. 3945, Springer, 81--96.
82. Tsukada, T. and Kobayashi, N. 2010. Untyped recursion schemes and infinite intersection types. In Proceedings of FOSSACS’10. Lecture Notes in Computer Science, vol. 6014, Springer, 343--357.
83. Turner, R. 1972. An infinite hierarchy of term languages - an approach to mathematical complexity. In Proceedings of ICALP. North-Holland, 593--608.
84. van Bakel, S. 1992. Complete restrictions of the intersection type discipline. Theoret. Comput. Sci. 102, 1, 135--163.
85. van Bakel, S. 1995. Intersection type assignment systems. Theoret. Comput. Sci. 151, 2, 385--435.
86. Wand, M. 1974. An algebraic formulation of the Chomsky hierarchy. In Category Theory Applied to Computation and Control, Lecture Notes in Computer Science, vol. 25, Springer, 209--213.
87. Wright, A. K. and Felleisen, M. 1994. A syntactic approach to type soundness. Inf. Comput. 115, 1, 38--94.
88. Yi, K. 1994. Compile-time detection of uncaught exceptions in Standard ML programs. In Proceedings of the 1st International Static Analysis Symposium (SAS’94). Lecture Notes in Computer Science, vol. 864, Springer, 238--254.

Index Terms

• Theory of computation

  • Logic

  • Semantics and reasoning

    • Program reasoning