Automatically disproving fair termination of higher-order functional programs

Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi

Research output: Contribution to journalArticlepeer-review

Abstract

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

Original languageEnglish
Pages (from-to)243-255
Number of pages13
JournalACM SIGPLAN Notices
Volume51
Issue number9
DOIs
Publication statusPublished - Sep 4 2016
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Automatically disproving fair termination of higher-order functional programs'. Together they form a unique fingerprint.

Cite this