Tachi Terauchi (JAIST)

Title: Temporal Verification of Higher-Order Functional Programs

Abstract: We present an automated approach to verifying arbitrary
omega-regular properties of higher-order functional programs.
Previous automated methods proposed for this class of programs
could only handle safety properties or termination, and our
approach is the first to be able to verify arbitrary omega-regular
liveness properties.

This is a joint work with Akihiro Murase (Nagoya U./Toshiba),
Naoki Kobayashi (U. Tokyo), Ryosuke Sato (U. Tokyo), and Hiroshi
Unno (U. Tsukuba)