Automatically disproving fair termination of higher-order functional programs

Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

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

Original languageEnglish
Title of host publicationICFP 2016 - Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
EditorsEijiro Sumii, Jacques Garrigue, Gabriele Keller
PublisherAssociation for Computing Machinery, Inc
Pages243-255
Number of pages13
ISBN (Print)9781450342193
DOIs
Publication statusPublished - Aug 4 2016
Externally publishedYes
Event21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016 - Nara, Japan
Duration: Sep 18 2016Sep 24 2016

Publication series

NameICFP 2016 - Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

Other

Other21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016
CountryJapan
CityNara
Period9/18/169/24/16

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Science Applications
  • Computational Theory and Mathematics

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

  • Cite this

    Watanabe, K., Sato, R., Tsukada, T., & Kobayashi, N. (2016). Automatically disproving fair termination of higher-order functional programs. In E. Sumii, J. Garrigue, & G. Keller (Eds.), ICFP 2016 - Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (pp. 243-255). (ICFP 2016 - Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming). Association for Computing Machinery, Inc. https://doi.org/10.1145/2951913.2951919