Model Checking Higher-Order Programs with Recursive Types

By Naoki Kobayashi and Atsushi Igarashi. In Proceedings of European Symposium on Programming (ESOP2013), volume 7792 of Springer LNCS, Rome, Italy, March, 2013.


Model checking of higher-order recursion schemes (HORS, for short) has been recently studied as a new promising technique for automated verification of higher-order programs. The previous HORS model checking could however deal with only simply-typed programs, so that its application was limited to functional programs. To deal with a broader range of programs such as object-oriented programs and multi- threaded programs, we extend HORS model checking to check properties of programs with recursive types. Although the extended model checking problem is undecidable, we develop a sound model-checking algorithm that is relatively complete with respect to a recursive intersection type system and prove its correctness. Preliminary results on the implemen- tation and applications to verification of object-oriented programs and multi-threaded programs are also reported.