Model-checking higher-order programs with recursive types. An extended version available from http://www-kb.is.s.u-tokyo.ac. jp/~koba/fjmc

Abstract. 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.