Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Tue 20 Sep 2016 13:55 - 14:20 at Noh Theater - Session 6 Chair(s): Johan Jeuring

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 Sep
Times are displayed in time zone: (GMT+09:00) Osaka, Sapporo, Tokyo change

13:30 - 14:45: Research Papers - Session 6 at Noh Theater
Chair(s): Johan JeuringUtrecht University
icfp-2016-papers13:30 - 13:55
Eric SeidelUniversity of California at San Diego, USA, Ranjit JhalaUniversity of California at San Diego, USA, Westley WeimerUniversity of Virginia, USA
icfp-2016-papers13:55 - 14:20
Keiichi WatanabeUniversity of Tokyo, Japan, Ryosuke SatoUniversity of Tokyo, Japan, Takeshi TsukadaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan
icfp-2016-papers14:20 - 14:45
Ralf JungMPI-SWS, Germany, Robbert KrebbersAarhus University, Denmark, Lars BirkedalAarhus University, Denmark, Derek DreyerMPI-SWS, Germany