Automatic termination verification for higher-order functional programs

Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi

研究成果: Conference contribution

25 被引用数 (Scopus)

抄録

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.

本文言語English
ホスト出版物のタイトル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
出版社Springer Verlag
ページ392-411
ページ数20
ISBN(印刷版)9783642548321
DOI
出版ステータスPublished - 2014
外部発表はい
イベント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
継続期間: 2014 4 52014 4 13

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
8410 LNCS
ISSN(印刷版)0302-9743
ISSN(電子版)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
国/地域France
CityGrenoble
Period14/4/514/4/13

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「Automatic termination verification for higher-order functional programs」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル