Temporal verification of higher-order functional programs

Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno

研究成果: Chapter in Book/Report/Conference proceedingConference contribution

12 被引用数 (Scopus)

抄録

We present an automated approach to verifying arbitrary omegaregular properties of higher-order functional programs. Previous automated methods proposed for this class of programs could only handle safety properties or termination, and our approach is the first to be able to verify arbitrary omega-regular liveness properties. Our approach is automata-theoretic, and extends our recent work on binary-reachability-based approach to automated termination verification of higher-order functional programs to fair termination published in ESOP 2014. In that work, we have shown that checking disjunctive well-foundedness of (the transitive closure of) the "calling relation" is sound and complete for termination. The extension to fair termination is tricky, however, because the straightforward extension that checks disjunctive well-foundedness of the fair calling relation turns out to be unsound, as we shall show in the paper. Roughly, our solution is to check fairness on the transition relation instead of the calling relation, and propagate the information to determine when it is necessary and sufficient to check for disjunctive well-foundedness on the calling relation. We prove that our approach is sound and complete. We have implemented a prototype of our approach, and confirmed that it is able to automatically verify liveness properties of some non-trivial higher-order programs.

本文言語英語
ホスト出版物のタイトルPOPL 2016 - Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
編集者Rupak Majumdar, Rastislav Bodik
出版社Association for Computing Machinery
ページ57-68
ページ数12
ISBN(電子版)9781450335492
DOI
出版ステータス出版済み - 1 11 2016
外部発表はい
イベント43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016 - St. Petersburg, 米国
継続期間: 1 20 20161 22 2016

出版物シリーズ

名前Conference Record of the Annual ACM Symposium on Principles of Programming Languages
20-22-January-2016
ISSN(印刷版)0730-8566

その他

その他43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016
国/地域米国
CitySt. Petersburg
Period1/20/161/22/16

All Science Journal Classification (ASJC) codes

  • ソフトウェア

フィンガープリント

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

引用スタイル