Naoki Kobayashi
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.
- Objective caml. http://caml.inria.fr/ocaml/.Google Scholar
- 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-two recursion schemes is decidable. In TLCA 2005, volume 3461 of LNCS, pages 39--54. Springer-Verlag, 2005. Google ScholarDigital Library
- 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. 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
- 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
- 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. Google ScholarDigital Library
- G. Boudol. On strong normalization and type inference in the intersection type discipline. Theor. Comput. Sci., 398(1-3):63--81, 2008. Google ScholarDigital Library
- 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.Google Scholar
- B. Courcelle. The monadic second-order logic of graphs IX: machines and their behaviours. Theoretical Computer Science, 151:125--162, 1995. Google ScholarDigital Library
- 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. 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
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. In ICALP 2005, volume 3580 of LNCS, pages 1450--1461. Springer-Verlag, 2005. Google ScholarDigital Library
- N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In Proc. of POPL, pages 416--428, 2009. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- X. Leroy and F. Pessaux. Type-based analysis of uncaught exceptions. ACM Trans. Prog. Lang. Syst., 22(2):340--377, 2000. Google ScholarDigital Library
- M. Might and O. Shivers. Exploiting reachability and cardinality in higher-order flow analysis. J. Funct. Program., 18(5-6):821--864, 2008. Google ScholarDigital Library
- F. Nielson, H.R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999. 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
- M.O. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Maths. Soc, 141:1--35, 1969.Google Scholar
- J. Rehof and T. Mogensen. Tractable constraints in finite semilattices. Science of Computer Programming, 35(2):191--221, 1999. Google ScholarDigital Library
- S.R.D. Rocca and B. Venneri. Principal type schemes for an extended type theory. Theor. Comput. Sci., 28:151--169, 1984.Google ScholarCross Ref
Index Terms
- Model-checking higher-order functions
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 ...
Model Checking Higher-Order Programs
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 ...
Accelerating Software Model Checking Based on Program Backbone
APPT 2013: Revised Selected Papers of the 10th International Symposium on Advanced Parallel Processing Technologies - Volume 8299Model checking technique has been gradually applied to verify the reliability of software systems. However, as to software with large scale and complex structure, the verification procedure suffers from the state space explosion, thus leading to a low ...
Comments