TY - JOUR
T1 - Automatically disproving fair termination of higher-order functional programs
AU - Watanabe, Keiichi
AU - Sato, Ryosuke
AU - Tsukada, Takeshi
AU - Kobayashi, Naoki
N1 - Funding Information:
We would like to thank Hiroshi Unno for discussions, and anonymous referees for useful comments. This work was supported by JSPS Kakenhi 15H05706.
Publisher Copyright:
© 2016 ACM.
PY - 2016/9/4
Y1 - 2016/9/4
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85084462634&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85084462634&partnerID=8YFLogxK
U2 - 10.1145/2951913.2951919
DO - 10.1145/2951913.2951919
M3 - Article
AN - SCOPUS:85084462634
VL - 51
SP - 243
EP - 255
JO - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)
JF - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)
SN - 1523-2867
IS - 9
ER -