Automating relatively complete verification of higher-order functional programs

Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi

Research output: Contribution to journalArticle

9 Citations (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)75-86
Number of pages12
JournalACM SIGPLAN Notices
Volume48
Issue number1
DOIs
Publication statusPublished - 2013 Jan 1
Externally publishedYes

Keywords

  • Higher-order programs
  • Relative completeness
  • Software model checking
  • Type inference

ASJC Scopus subject areas

  • Computer Science(all)

Cite this