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
Externally publishedYes
Event40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013 - Rome, Italy
Duration: 2013 Jan 232013 Jan 25

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) https://doi.org/10.1145/2429069.2429081

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

POPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2013. p. 75-86.

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

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, 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy, 13/1/23. https://doi.org/10.1145/2429069.2429081
Unno H, Terauchi T, Kobayashi N. 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. 2013. p. 75-86 https://doi.org/10.1145/2429069.2429081
Unno, Hiroshi ; Terauchi, Tachio ; Kobayashi, Naoki. / Automating relatively complete verification of higher-order functional programs. POPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2013. pp. 75-86
@inproceedings{e0feb53e8cda4dd2977f3ccdbecd2695,
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",
doi = "10.1145/2429069.2429081",
language = "English",
isbn = "9781450318327",
pages = "75--86",
booktitle = "POPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",

}

TY - GEN

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

AU - Unno, Hiroshi

AU - Terauchi, Tachio

AU - Kobayashi, Naoki

PY - 2013

Y1 - 2013

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=84874181407&partnerID=8YFLogxK

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

U2 - 10.1145/2429069.2429081

DO - 10.1145/2429069.2429081

M3 - Conference contribution

SN - 9781450318327

SP - 75

EP - 86

BT - POPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

ER -