Automatically Disproving Fair Termination of Higher-Order Functional Programs

作者：Watanabe Keiichi^*; Sato Ryosuke; Tsukada Takeshi; Kobayashi Naoki

来源：ACM Sigplan Notices, 2016, 51(9): 243-255.

DOI：10.1145/2951913.2951919

• Automatic Verification
• Fair Termination
• Higher-Order Programs
• Predicate Abstraction
• Higher-Order Model Checking
• CEGAR

We propose an automated method for disproving fair termination of higher-order functional programs, which is complementary to Murase et al.'s recent method for proving fair termination. A program is said to be fair terminating if it has no infinite execution trace that satisfies a given fairness constraint. Fair termination is an important property because program verification problems for arbitrary omega-regular temporal properties can be transformed to those of fair termination. Our method reduces the problem of disproving fair termination to higher-order model checking by using predicate abstraction and CEGAR. Given a program, we convert it to an abstract program that generates an approximation of the (possibly infinite) execution traces of the original program, so that the original program has a fair infinite execution trace if the tree generated by the abstract program satisfies a certain property. The method is a non-trivial extension of Kuwahara et al.'s method for disproving plain termination. We implemented a prototype verification tool based on our method and confirmed its effectiveness.

• 出版日期2016-9