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
Externally publishedYes

Keywords

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

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

Automating relatively complete verification of higher-order functional programs. / Unno, Hiroshi; Terauchi, Tachio; Kobayashi, Naoki.

In: ACM SIGPLAN Notices, Vol. 48, No. 1, 01.2013, p. 75-86.

Research output: Contribution to journalArticle

@article{a4abb04cea3146728596968f562d3b8c,
title = "Automating relatively complete verification of higher-order functional programs",
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.",
keywords = "Higher-order programs, Relative completeness, Software model checking, Type inference",
author = "Hiroshi Unno and Tachio Terauchi and Naoki Kobayashi",
year = "2013",
month = "1",
doi = "10.1145/2480359.2429081",
language = "English",
volume = "48",
pages = "75--86",
journal = "SIGPLAN Notices (ACM Special Interest Group on Programming Languages)",
issn = "0362-1340",
publisher = "Association for Computing Machinery (ACM)",
number = "1",

}

TY - JOUR

T1 - Automating relatively complete verification of higher-order functional programs

AU - Unno, Hiroshi

AU - Terauchi, Tachio

AU - Kobayashi, Naoki

PY - 2013/1

Y1 - 2013/1

N2 - 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.

AB - 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.

KW - Higher-order programs

KW - Relative completeness

KW - Software model checking

KW - Type inference

UR - http://www.scopus.com/inward/record.url?scp=84877890900&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84877890900&partnerID=8YFLogxK

U2 - 10.1145/2480359.2429081

DO - 10.1145/2480359.2429081

M3 - Article

AN - SCOPUS:84877890900

VL - 48

SP - 75

EP - 86

JO - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)

JF - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)

SN - 0362-1340

IS - 1

ER -