Automating relatively complete verification of higher-order functional programs

Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

15 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
Title of host publicationPOPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages75-86
Number of pages12
DOIs
Publication statusPublished - 2013 Feb 26
Event40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013 - Rome, Italy
Duration: 2013 Jan 232013 Jan 25

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Other

Other40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013
CountryItaly
CityRome
Period13/1/2313/1/25

Keywords

  • higher-order programs
  • relative completeness
  • software model checking
  • type inference

ASJC Scopus subject areas

  • Software

Cite this

Unno, H., Terauchi, T., & Kobayashi, N. (2013). Automating relatively complete verification of higher-order functional programs. In POPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 75-86). (Conference Record of the Annual ACM Symposium on Principles of Programming Languages). https://doi.org/10.1145/2429069.2429081