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

3 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

Other

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

Fingerprint

Model checking

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Science Applications
  • Computational Theory and Mathematics

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). Association for Computing Machinery, Inc. https://doi.org/10.1145/2951913.2951919

Automatically disproving fair termination of higher-order functional programs. / Watanabe, Keiichi; Sato, Ryosuke; Tsukada, Takeshi; Kobayashi, Naoki.

ICFP 2016 - Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. ed. / Eijiro Sumii; Jacques Garrigue; Gabriele Keller. Association for Computing Machinery, Inc, 2016. p. 243-255.

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

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. Association for Computing Machinery, Inc, pp. 243-255, 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, 9/18/16. https://doi.org/10.1145/2951913.2951919
Watanabe K, Sato R, Tsukada T, Kobayashi N. Automatically disproving fair termination of higher-order functional programs. In Sumii E, Garrigue J, Keller G, editors, ICFP 2016 - Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. Association for Computing Machinery, Inc. 2016. p. 243-255 https://doi.org/10.1145/2951913.2951919
Watanabe, Keiichi ; Sato, Ryosuke ; Tsukada, Takeshi ; Kobayashi, Naoki. / Automatically disproving fair termination of higher-order functional programs. ICFP 2016 - Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. editor / Eijiro Sumii ; Jacques Garrigue ; Gabriele Keller. Association for Computing Machinery, Inc, 2016. pp. 243-255
@inproceedings{f23b58f854da4d76bb62ada269d1b73d,
title = "Automatically disproving fair termination of higher-order functional programs",
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.",
author = "Keiichi Watanabe and Ryosuke Sato and Takeshi Tsukada and Naoki Kobayashi",
year = "2016",
month = "8",
day = "4",
doi = "10.1145/2951913.2951919",
language = "English",
isbn = "9781450342193",
pages = "243--255",
editor = "Eijiro Sumii and Jacques Garrigue and Gabriele Keller",
booktitle = "ICFP 2016 - Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming",
publisher = "Association for Computing Machinery, Inc",

}

TY - GEN

T1 - Automatically disproving fair termination of higher-order functional programs

AU - Watanabe, Keiichi

AU - Sato, Ryosuke

AU - Tsukada, Takeshi

AU - Kobayashi, Naoki

PY - 2016/8/4

Y1 - 2016/8/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 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.

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

UR - http://www.scopus.com/inward/record.url?scp=85030572142&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85030572142&partnerID=8YFLogxK

U2 - 10.1145/2951913.2951919

DO - 10.1145/2951913.2951919

M3 - Conference contribution

AN - SCOPUS:85030572142

SN - 9781450342193

SP - 243

EP - 255

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

A2 - Sumii, Eijiro

A2 - Garrigue, Jacques

A2 - Keller, Gabriele

PB - Association for Computing Machinery, Inc

ER -