Combining higher-order model checking with refinement type inference

Ryosuke Sato, Naoki Iwayama, Naoki Kobayashi

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

1 Citation (Scopus)

Abstract

There have been two major approaches to fully automated verification of higher-order functional programs: higher-order model checking and refinement type inference. The former approach is precise, but suffers from a bottleneck in the predicate discovery phase. The latter approach is generally faster than the former, thanks to the recent advances in constrained Horn clause (CHC) solving, but is imprecise, in that it rejects some valid programs. To take the best of the two approaches, we refine the higher-order model checking approach, by employing CHC solving in the predicate discovery phase. We have implemented the new approach and confirmed that the new system can verify more programs than those based on the previous two approaches.

Original languageEnglish
Title of host publicationPEPM 2019 - Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2019
EditorsManuel Hermenegildo, Atsushi Igarashi
PublisherAssociation for Computing Machinery, Inc
Pages47-53
Number of pages7
ISBN (Electronic)9781450362269
DOIs
Publication statusPublished - Jan 14 2019
Event2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2019, in affiliation with the annual Symposium on Principles of Programming Languages, POPL 2019 - Cascais, Portugal
Duration: Jan 14 2019Jan 15 2019

Publication series

NamePEPM 2019 - Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2019

Conference

Conference2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2019, in affiliation with the annual Symposium on Principles of Programming Languages, POPL 2019
CountryPortugal
CityCascais
Period1/14/191/15/19

All Science Journal Classification (ASJC) codes

  • Computer Graphics and Computer-Aided Design
  • Computer Vision and Pattern Recognition
  • Software

Fingerprint Dive into the research topics of 'Combining higher-order model checking with refinement type inference'. Together they form a unique fingerprint.

  • Cite this

    Sato, R., Iwayama, N., & Kobayashi, N. (2019). Combining higher-order model checking with refinement type inference. In M. Hermenegildo, & A. Igarashi (Eds.), PEPM 2019 - Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2019 (pp. 47-53). (PEPM 2019 - Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2019). Association for Computing Machinery, Inc. https://doi.org/10.1145/3294032.3294081