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
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
T2 - 23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014
Y2 - 5 April 2014 through 13 April 2014
ER -