skip to main content
research-article

Types and higher-order recursion schemes for verification of higher-order programs

Published:21 January 2009Publication History
Skip Abstract Section

Abstract

We 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 transformed to an HORS that generates a tree representing all the possible event sequences of the program, and then the HORS is model-checked. Unlike most of the previous methods for verification of higher-order programs, our verification method is sound and complete. Moreover, this new verification framework allows a smooth integration of abstract model checking techniques into verification of higher-order programs. We also present a type-based verification algorithm for HORS's. The algorithm can deal with only a fragment of the properties expressed by modal mu-calculus, but the algorithm and its correctness proof are (arguably) much simpler than those of Ong's game-semantics-based algorithm. Moreover, while the HORS model checking problem is n-EXPTIME in general, our algorithm is linear in the size of HORS, under the assumption that the sizes of types and specification formulas are bounded by a constant.

References

  1. K. Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science, 3(3), 2007.Google ScholarGoogle Scholar
  2. K. Aehlig, J. G. de Miranda, and C.-H. L. Ong. The monadic second order theory of trees given by arbitrary level--tworecursion schemes is decidable. In TLCA 2005, volume 3461 of LNCS, pages 39--54.Springer-Verlag, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. T. Ball, R. Majumdar, T. D. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In PLDI 2001, pages 203--213, 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. T. Ball and S. K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL, pages 1--3, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. 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. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. S. Chaki, S. Rajamani, and J. Rehof. Types as models: Model checking message-passing programs. In Proc. of POPL, pages 45--57, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. B. Cook, A. Gotsman, A. Podelski, A. Rybalchenko, and M. Y. Vardi. Proving that programs eventually do something good. In Proc. of POPL, pages 265--276, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. R. DeLine and M. Fähndrich. Adoption and focus: Practical linear types for imperative programming. In Proc. of PLDI, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. E. A. Emerson and C. S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In FOCS 1991, pages 368--377, 1991. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. J. Field, D. Goyal, G.a Ramalingam, and E. Yahav. Typestate verification: Abstraction techniques and complexity Sci. Comput. Program., 58(1-2):57--82, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. S. J. Fink, E. Yahav, N. Dor, G. Ramalingam, and E. Geay. Effective typestate verification in the presence of aliasing. ACM Trans. Softw. Eng. Methodol., 17(2), 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. J. S. Foster, T. Terauchi, and A. Aiken. ACM Trans. Softw. Eng. Methodol., 17(2), 2008. In Proc. of PLDI, pages 1--12, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. C. Haack and J. B. Wells. Type error slicing in implicitly typed higher-order languages. Science of Computer Programming, 50(1-3):189--224, 2004. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. M. Hague and C.-H. L. Ong. Symbolic backwards-reachability analysis for higher-order pushdown In FoSSaCS 2007, volume 4423 of LNCS, pages 213--227. Springer-Verlag, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  15. N. Heintze and D. A. McAllester. Linear-time subtransitive control flow analysis. In Proc. of PLDI, pages 261--272, 1997. Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Proc. of POPL, pages 58--70, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. H. Hosoya, J. Vouillon, and B. C. Pierce. Regular expression types for xml. ACM Trans. Program. Lang. Syst., 27(1):46--90, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. A. Igarashi and N. Kobayashi. A generic type system for the pi-calculus. Theor. Comput. Sci., 311(1-3):121--163, 2004. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. 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. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. 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. Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. D. Kikuchi and N. Kobayashi. Type-based verification of correspondence assertions for communication protocols. In Proceedings of APLAS 2007, volume 4807 of LNCS, pages 191--205. Springer-Verlag, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. T. Knapik, D. Niwinski, and P. Urzyczyn. Deciding monadic theories of hyperalgebraic trees. Deciding monadic theories of hyperalgebraic trees. Springer-Verlag, 2001.Google ScholarGoogle Scholar
  23. 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. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. T. Knapik, D. Niwinski, P. Urzyczyn, and I. Walukiewicz. Unsafe grammars and panic automata. Unsafe grammars and panic automata. Springer-Verlag, 2005.Google ScholarGoogle Scholar
  25. N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. An extended version, available from http://www.kb.ecei.tohoku.ac.jp/ koba/papers/hors.pdf, 2008.Google ScholarGoogle Scholar
  26. P. Lam, V. Kuncak, and M. C. Rinard. Generalized typestate checking for data structure consistency. In VMCAI 2005, volume 3385 of LNCS, pages 430--447.Springer-Verlag, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  27. M. Naik. A type system equivalent to a model checker. Master Thesis, Purdue University.Google ScholarGoogle Scholar
  28. M. Naik and J. Palsberg. A type system equivalent to a model checker. In ESOP 2005, volume 3444 of LNCS, pages 374--388. Springer-Verlag, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  29. 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. Google ScholarGoogle ScholarDigital LibraryDigital Library
  30. J. Rehof and T. Mogensen. Tractable constraints in finite semilattices. Science of Computer Programming, 35(2):191--221, 1999. Google ScholarGoogle ScholarDigital LibraryDigital Library
  31. P. M. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI 2008, pages 159--169, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  32. R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. Transactions on Software Engineering, 12(1):157--171, 1986. Google ScholarGoogle ScholarDigital LibraryDigital Library
  33. W. Thomas. Languages, automata, and logic. In Handbook of formal languages, vol. 3, pages 389--455, 1997. Google ScholarGoogle ScholarCross RefCross Ref
  34. H. Unno and N. Kobayashi. On-demand refinement of dependent types. In Proceedings of FLOPS 2008, volume 4989 of LNCS, pages 81--96. Springer-Verlag, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Types and higher-order recursion schemes for verification of higher-order programs

              Recommendations

              Comments

              Login options

              Check if you have access through your login credentials or your institution to get full access on this article.

              Sign in

              Full Access

              • Published in

                cover image ACM SIGPLAN Notices
                ACM SIGPLAN Notices  Volume 44, Issue 1
                POPL '09
                January 2009
                453 pages
                ISSN:0362-1340
                EISSN:1558-1160
                DOI:10.1145/1594834
                Issue’s Table of Contents
                • cover image ACM Conferences
                  POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
                  January 2009
                  464 pages
                  ISBN:9781605583792
                  DOI:10.1145/1480881

                Copyright © 2009 ACM

                Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

                Publisher

                Association for Computing Machinery

                New York, NY, United States

                Publication History

                • Published: 21 January 2009

                Check for updates

                Qualifiers

                • research-article

              PDF Format

              View or Download as a PDF file.

              PDF

              eReader

              View online with eReader.

              eReader