Model-Checking Higher-Order Programs with Recursive Types

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 multithreaded 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 implementation and applications to verification of object-oriented programs and multi-threaded programs are also reported.