Automating relatively complete verification of higher-order functional programs

この論文にアクセスする

抄録

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.

収録刊行物

  • Proceeding POPL '13 Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

    Proceeding POPL '13 Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 75-86, 2013-01

    ACM

キーワード

各種コード

  • NII論文ID(NAID)
    120006669372
  • 本文言語コード
    ENG
  • 資料種別
    conference paper
  • データ提供元
    IR 
ページトップへ