Model-checking higher-order functions

ABSTRACT

We propose a novel type-based model checking algorithm for higher-order recursion schemes. As shown by Kobayashi, verification problems of higher-order functional programs can easily be translated into model checking problems of recursion schemes. Thus, the model checking algorithm serves as a basis for verification of higher-order functional programs. To our knowledge, this is the first practical algorithm for model checking recursion schemes: all the previous algorithms always suffer from the n-EXPTIME bottleneck, not only in the worst, and there was no implementation of the algorithms. We have implemented a model checker for recursion schemes based on the proposed algorithm, and applied it to verification of functional programs, including reachability, flow analysis and resource usage verification problems. According to our experiments, the model checker is surprisingly fast: it could automatically verify a number of small but tricky higher-order functional programs in less than a second.

REFERENCES

• 1: Objective caml. http://caml.inria.fr/ocaml/.
• 2: K. Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science, 3(3), 2007.
• 3: K. Aehlig, J.G. de Miranda, and C.-H.L. Ong. The monadic second order theory of trees given by arbitrary level-two recursion schemes is decidable. In TLCA 2005, volume 3461 of LNCS, pages 39--54. Springer-Verlag, 2005.
• 4: A. Bakewell and D.R. Ghica. On-the-fly techniques for game-based software model checking. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, volume 4963 of LNCS, pages 78--92. Springer-Verlag, 2008.
• 5: T. Ball, R. Majumdar, T.D. Millstein, and S.K. Rajamani. Automatic predicate abstraction of C programs. In PLDI 2001, pages 203--213, 2001.
• 6: D. Beyer, T.A. Henzinger, R. Jhala, and R. Majumdar. The software model checker blast. International Journal on Software Tools for Technology Transfer, 9(5-6):505--525, 2007.
• 7: M. Blume, U.A. Acar, and W. Chae. Exception handlers as extensible cases. In Proceedings of APLAS 2008, volume 5356 of LNCS, pages 273--289. Springer-Verlag, 2008.
• 8: G. Boudol. On strong normalization and type inference in the intersection type discipline. Theor. Comput. Sci., 398(1-3):63--81, 2008.
• 9: M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Principal type schemes and lambda-calculus semantics. In Essays on Combinatory Logic, Lambda Calculus, and Foundation, pages 535--560. Academic Press, 1980.
• 10: B. Courcelle. The monadic second-order logic of graphs IX: machines and their behaviours. Theoretical Computer Science, 151:125--162, 1995.
• 11: M. Hague, A. Murawski, C.-H.L. Ong, and O. Serre. Collapsible pushdown automata and recursion schemes. In Proceedings of 23rd Annual IEEE Symposium on Logic in Computer Science, pages 452--461. IEEE Computer Society, 2008.
• 12: A. Igarashi and N. Kobayashi. Resource usage analysis. ACM Trans. Prog. Lang. Syst., 27(2):264--313, 2005. Preliminary summary appeared in Proceedings of POPL 2002.
• 13: F. Iwama, A. Igarashi, and N. Kobayashi. Resource usage analysis for a functional language with exceptions. In Proceedings of ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program Manipulation (PEPM 2006), pages 38--47. ACM Press, 2006.
• 14: A.J. Kfoury and J.B. Wells. Principality and type inference for intersection types using expansion variables. Theor. Comput. Sci., 311(1-3):1--70, 2004.
• 15: T. Knapik, D. Niwinski, and P. Urzyczyn. Deciding monadic theories of hyperalgebraic trees. In TLCA 2001, volume 2044 of LNCS, pages 253--267. Springer-Verlag, 2001.
• 16: T. Knapik, D. Niwinski, and P. Urzyczyn. Higher-order pushdown trees are easy. In FoSSaCS 2002, volume 2303 of LNCS, pages 205--222. Springer-Verlag, 2002.
• 17: T. Knapik, D. Niwinski, P. Urzyczyn, and I. Walukiewicz. Unsafe grammars and panic automata. In ICALP 2005, volume 3580 of LNCS, pages 1450--1461. Springer-Verlag, 2005.
• 18: N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In Proc. of POPL, pages 416--428, 2009.
• 19: N. Kobayashi and C.-H.L. Ong. Complexity of model checking recursion schemes for fragments of the modal mu-calculus. In Proceedings of ICALP 2009, LNCS. Springer-Verlag, 2009.
• 20: N. Kobayashi and C.-H.L. Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In Proceedings of LICS 2009. IEEE Computer Society Press, 2009.
• 21: X. Leroy and F. Pessaux. Type-based analysis of uncaught exceptions. ACM Trans. Prog. Lang. Syst., 22(2):340--377, 2000.
• 22: M. Might and O. Shivers. Exploiting reachability and cardinality in higher-order flow analysis. J. Funct. Program., 18(5-6):821--864, 2008.
• 23: F. Nielson, H.R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.
• 24: C.-H.L. Ong. On model-checking trees generated by higher-order recursion schemes. In LICS 2006, pages 81--90. IEEE Computer Society Press, 2006.
• 25: M.O. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Maths. Soc, 141:1--35, 1969.
• 26: J. Rehof and T. Mogensen. Tractable constraints in finite semilattices. Science of Computer Programming, 35(2):191--221, 1999.
• 27: S.R.D. Rocca and B. Venneri. Principal type schemes for an extended type theory. Theor. Comput. Sci., 28:151--169, 1984.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Verification

Keywords:
higher-order functions, model checking, program verification, recursion schemes