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