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.
- K. Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science, 3(3), 2007.Google Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- T. Ball and S. K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL, pages 1--3, 2002. Google ScholarDigital Library
- 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 ScholarDigital Library
- S. Chaki, S. Rajamani, and J. Rehof. Types as models: Model checking message-passing programs. In Proc. of POPL, pages 45--57, 2002. Google ScholarDigital Library
- 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 ScholarDigital Library
- R. DeLine and M. Fähndrich. Adoption and focus: Practical linear types for imperative programming. In Proc. of PLDI, 2002. Google ScholarDigital Library
- E. A. Emerson and C. S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In FOCS 1991, pages 368--377, 1991. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- N. Heintze and D. A. McAllester. Linear-time subtransitive control flow analysis. In Proc. of PLDI, pages 261--272, 1997. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Proc. of POPL, pages 58--70, 2002. Google ScholarDigital Library
- H. Hosoya, J. Vouillon, and B. C. Pierce. Regular expression types for xml. ACM Trans. Program. Lang. Syst., 27(1):46--90, 2005. Google ScholarDigital Library
- A. Igarashi and N. Kobayashi. A generic type system for the pi-calculus. Theor. Comput. Sci., 311(1-3):121--163, 2004. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- T. Knapik, D. Niwinski, and P. Urzyczyn. Deciding monadic theories of hyperalgebraic trees. Deciding monadic theories of hyperalgebraic trees. Springer-Verlag, 2001.Google Scholar
- 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 ScholarDigital Library
- T. Knapik, D. Niwinski, P. Urzyczyn, and I. Walukiewicz. Unsafe grammars and panic automata. Unsafe grammars and panic automata. Springer-Verlag, 2005.Google Scholar
- 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 Scholar
- 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 ScholarDigital Library
- M. Naik. A type system equivalent to a model checker. Master Thesis, Purdue University.Google Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- J. Rehof and T. Mogensen. Tractable constraints in finite semilattices. Science of Computer Programming, 35(2):191--221, 1999. Google ScholarDigital Library
- P. M. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI 2008, pages 159--169, 2008. Google ScholarDigital Library
- 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 ScholarDigital Library
- W. Thomas. Languages, automata, and logic. In Handbook of formal languages, vol. 3, pages 389--455, 1997. Google ScholarCross Ref
- 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 ScholarDigital Library
Index Terms
Types and higher-order recursion schemes for verification of higher-order programs
Recommendations
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 ...
On the relationship between higher-order recursion schemes and higher-order fixpoint logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesWe study the relationship between two kinds of higher-order extensions
of model checking: HORS model checking, where models are extended to
higher-order recursion schemes, and HFL model checking, where the
logic is extedned to higher-order modal ...
On the relationship between higher-order recursion schemes and higher-order fixpoint logic
POPL '17We study the relationship between two kinds of higher-order extensions
of model checking: HORS model checking, where models are extended to
higher-order recursion schemes, and HFL model checking, where the
logic is extedned to higher-order modal ...
Comments