We propose a new verification method for temporal properties ofhigher-order functional programs, which takes advantage of Ong'srecent result on the decidability of the model-checking problemfor higher-order recursion schemes (HORS's). A program is trans-formed to an HORS that generates a tree representing all the possi-ble event sequences of the program, and then the HORS is model-checked. Unlike most of the previous methods for verification ofhigher-order programs, our verification method is sound and com-plete. Moreover, this new verification framework allows a smoothintegration of abstract model checking techniques into verificationof higher-order programs. We also present a type-based verificationalgorithm for HORS's. The algorithm can deal with only a frag-ment of the properties expressed by modal μ-calculus, but the al-gorithm and its correctness proof are (arguably) much simpler thanthose of Ong's game-semantics-based algorithm. Moreover, whilethe HORS model checking problem is n-EXPTIME in general, ouralgorithm is linear in the size of HORS, under the assumption thatthe sizes of types and specifications are bounded by a constant.
展开▼
