Automating relatively complete verification of higher-order functional programs

Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi

研究成果: Article査読

9 被引用数 (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
ページ(範囲)75-86
ページ数12
ジャーナルACM SIGPLAN Notices
48
1
DOI
出版ステータスPublished - 2013 1
外部発表はい

ASJC Scopus subject areas

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

引用スタイル