Automatic termination verification for higher-order functional programs

Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi

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

17 Citations (Scopus)

Abstract

We present an automated approach to verifying termination of higher-order functional programs. Our approach adopts the idea from the recent work on termination verification via transition invariants (a.k.a. binary reachability analysis), and is fully automated. Our approach is able to soundly handle the subtle aspects of higher-order programs, including partial applications, indirect calls, and ranking functions over function closure values. In contrast to the previous approaches to automated termination verification for functional programs, our approach is sound and complete, relative to the soundness and completeness of the underlying reachability analysis and ranking function inference. We have implemented a prototype of our approach for a subset of the OCaml language, and we have confirmed that it is able to automatically verify termination of some non-trivial higher-order programs.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings
PublisherSpringer Verlag
Pages392-411
Number of pages20
Volume8410 LNCS
ISBN (Print)9783642548321
DOIs
Publication statusPublished - 2014
Externally publishedYes
Event23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014 - Grenoble, France
Duration: 2014 Apr 52014 Apr 13

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8410 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014
CountryFrance
CityGrenoble
Period14/4/514/4/13

Fingerprint

Termination
Higher Order
Ranking Function
Reachability Analysis
Soundness
Acoustic waves
Completeness
Closure
Prototype
Binary
Verify
Partial
Subset
Invariant

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Kuwahara, T., Terauchi, T., Unno, H., & Kobayashi, N. (2014). Automatic termination verification for higher-order functional programs. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings (Vol. 8410 LNCS, pp. 392-411). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8410 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-642-54833-8_21

Automatic termination verification for higher-order functional programs. / Kuwahara, Takuya; Terauchi, Tachio; Unno, Hiroshi; Kobayashi, Naoki.

Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings. Vol. 8410 LNCS Springer Verlag, 2014. p. 392-411 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8410 LNCS).

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

Kuwahara, T, Terauchi, T, Unno, H & Kobayashi, N 2014, Automatic termination verification for higher-order functional programs. in Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings. vol. 8410 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8410 LNCS, Springer Verlag, pp. 392-411, 23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, 14/4/5. https://doi.org/10.1007/978-3-642-54833-8_21
Kuwahara T, Terauchi T, Unno H, Kobayashi N. Automatic termination verification for higher-order functional programs. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings. Vol. 8410 LNCS. Springer Verlag. 2014. p. 392-411. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-54833-8_21
Kuwahara, Takuya ; Terauchi, Tachio ; Unno, Hiroshi ; Kobayashi, Naoki. / Automatic termination verification for higher-order functional programs. Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings. Vol. 8410 LNCS Springer Verlag, 2014. pp. 392-411 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{f0ebdb0c93e84cae9e63885f4e958173,
title = "Automatic termination verification for higher-order functional programs",
abstract = "We present an automated approach to verifying termination of higher-order functional programs. Our approach adopts the idea from the recent work on termination verification via transition invariants (a.k.a. binary reachability analysis), and is fully automated. Our approach is able to soundly handle the subtle aspects of higher-order programs, including partial applications, indirect calls, and ranking functions over function closure values. In contrast to the previous approaches to automated termination verification for functional programs, our approach is sound and complete, relative to the soundness and completeness of the underlying reachability analysis and ranking function inference. We have implemented a prototype of our approach for a subset of the OCaml language, and we have confirmed that it is able to automatically verify termination of some non-trivial higher-order programs.",
author = "Takuya Kuwahara and Tachio Terauchi and Hiroshi Unno and Naoki Kobayashi",
year = "2014",
doi = "10.1007/978-3-642-54833-8_21",
language = "English",
isbn = "9783642548321",
volume = "8410 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "392--411",
booktitle = "Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Automatic termination verification for higher-order functional programs

AU - Kuwahara, Takuya

AU - Terauchi, Tachio

AU - Unno, Hiroshi

AU - Kobayashi, Naoki

PY - 2014

Y1 - 2014

N2 - We present an automated approach to verifying termination of higher-order functional programs. Our approach adopts the idea from the recent work on termination verification via transition invariants (a.k.a. binary reachability analysis), and is fully automated. Our approach is able to soundly handle the subtle aspects of higher-order programs, including partial applications, indirect calls, and ranking functions over function closure values. In contrast to the previous approaches to automated termination verification for functional programs, our approach is sound and complete, relative to the soundness and completeness of the underlying reachability analysis and ranking function inference. We have implemented a prototype of our approach for a subset of the OCaml language, and we have confirmed that it is able to automatically verify termination of some non-trivial higher-order programs.

AB - We present an automated approach to verifying termination of higher-order functional programs. Our approach adopts the idea from the recent work on termination verification via transition invariants (a.k.a. binary reachability analysis), and is fully automated. Our approach is able to soundly handle the subtle aspects of higher-order programs, including partial applications, indirect calls, and ranking functions over function closure values. In contrast to the previous approaches to automated termination verification for functional programs, our approach is sound and complete, relative to the soundness and completeness of the underlying reachability analysis and ranking function inference. We have implemented a prototype of our approach for a subset of the OCaml language, and we have confirmed that it is able to automatically verify termination of some non-trivial higher-order programs.

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

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

U2 - 10.1007/978-3-642-54833-8_21

DO - 10.1007/978-3-642-54833-8_21

M3 - Conference contribution

AN - SCOPUS:84900547825

SN - 9783642548321

VL - 8410 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 392

EP - 411

BT - Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings

PB - Springer Verlag

ER -