Automatically Disproving Fair Termination of Higher-Order Functional Programs
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.
Tue 20 SepDisplayed time zone: Osaka, Sapporo, Tokyo change
13:30 - 14:45 | |||
13:30 25mTalk | Dynamic Witnesses for Static Type Errors (or, Ill-Typed Programs Usually Go Wrong) Research Papers Eric Seidel University of California at San Diego, USA, Ranjit Jhala University of California at San Diego, USA, Westley Weimer University of Virginia, USA DOI | ||
13:55 25mTalk | Automatically Disproving Fair Termination of Higher-Order Functional Programs Research Papers Keiichi Watanabe University of Tokyo, Japan, Ryosuke Sato University of Tokyo, Japan, Takeshi Tsukada University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan DOI | ||
14:20 25mTalk | Higher-Order Ghost State Research Papers Ralf Jung MPI-SWS, Germany, Robbert Krebbers Aarhus University, Denmark, Lars Birkedal Aarhus University, Denmark, Derek Dreyer MPI-SWS, Germany DOI | ||