Automating relatively complete verification of higher-order functional programs

Hiroshi Unno*, Tachio Terauchi, Naoki Kobayashi

*この研究の対応する著者

研究成果: Conference contribution

27 被引用数 (Scopus)

抄録

We present an automated approach to relatively completely verifying safety (i.e., reachability) property of higher-order functional programs. Our contribution is two-fold. First, we extend the refinement type system framework employed in the recent work on (incomplete) automated higher-order verification by drawing on the classical work on relatively complete "Hoare logic like" program logic for higher-order procedural languages. Then, by adopting the recently proposed techniques for solving constraints over quantified first-order logic formulas, we develop an automated type inference method for the type system, thereby realizing an automated relatively complete verification of higher-order programs.

本文言語English
ホスト出版物のタイトルPOPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
ページ75-86
ページ数12
DOI
出版ステータスPublished - 2013
外部発表はい
イベント40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013 - Rome, Italy
継続期間: 2013 1月 23 → 2013 1月 25

出版物シリーズ

名前Conference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN（印刷版）0730-8566

Other

Other40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013
国/地域Italy
CityRome
Period13/1/23 → 13/1/25

ASJC Scopus subject areas

  • ソフトウェア

文献へのアクセス

他のファイルとリンク

引用スタイル