Combining higher-order model checking with refinement type inference

Ryosuke Sato, Naoki Iwayama, Naoki Kobayashi

研究成果: 著書/レポートタイプへの貢献会議での発言

抄録

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.

元の言語英語
ホスト出版物のタイトルPEPM 2019 - Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2019
編集者Manuel Hermenegildo, Atsushi Igarashi
出版者Association for Computing Machinery, Inc
ページ47-53
ページ数7
ISBN(電子版)9781450362269
DOI
出版物ステータス出版済み - 1 14 2019
イベント2019 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, ポルトガル
継続期間: 1 14 20191 15 2019

出版物シリーズ

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

会議

会議2019 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
期間1/14/191/15/19

Fingerprint

Model checking

All Science Journal Classification (ASJC) codes

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

これを引用

Sato, R., Iwayama, N., & Kobayashi, N. (2019). Combining higher-order model checking with refinement type inference. : M. Hermenegildo, & A. Igarashi (版), 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

Combining higher-order model checking with refinement type inference. / Sato, Ryosuke; Iwayama, Naoki; Kobayashi, Naoki.

PEPM 2019 - Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2019. 版 / Manuel Hermenegildo; Atsushi Igarashi. Association for Computing Machinery, Inc, 2019. p. 47-53 (PEPM 2019 - Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2019).

研究成果: 著書/レポートタイプへの貢献会議での発言

Sato, R, Iwayama, N & Kobayashi, N 2019, Combining higher-order model checking with refinement type inference. : M Hermenegildo & A Igarashi (版), PEPM 2019 - Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2019. 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, pp. 47-53, 2019 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, ポルトガル, 1/14/19. https://doi.org/10.1145/3294032.3294081
Sato R, Iwayama N, Kobayashi N. Combining higher-order model checking with refinement type inference. : Hermenegildo M, Igarashi A, 編集者, 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. 2019. p. 47-53. (PEPM 2019 - Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2019). https://doi.org/10.1145/3294032.3294081
Sato, Ryosuke ; Iwayama, Naoki ; Kobayashi, Naoki. / Combining higher-order model checking with refinement type inference. PEPM 2019 - Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2019. 編集者 / Manuel Hermenegildo ; Atsushi Igarashi. Association for Computing Machinery, Inc, 2019. pp. 47-53 (PEPM 2019 - Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2019).
@inproceedings{e63d1479406a439e8d6970f9be5b73f7,
title = "Combining higher-order model checking with refinement type inference",
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.",
author = "Ryosuke Sato and Naoki Iwayama and Naoki Kobayashi",
year = "2019",
month = "1",
day = "14",
doi = "10.1145/3294032.3294081",
language = "English",
series = "PEPM 2019 - Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2019",
publisher = "Association for Computing Machinery, Inc",
pages = "47--53",
editor = "Manuel Hermenegildo and Atsushi Igarashi",
booktitle = "PEPM 2019 - Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2019",

}

TY - GEN

T1 - Combining higher-order model checking with refinement type inference

AU - Sato, Ryosuke

AU - Iwayama, Naoki

AU - Kobayashi, Naoki

PY - 2019/1/14

Y1 - 2019/1/14

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

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

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

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

U2 - 10.1145/3294032.3294081

DO - 10.1145/3294032.3294081

M3 - Conference contribution

AN - SCOPUS:85061839927

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

SP - 47

EP - 53

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

A2 - Hermenegildo, Manuel

A2 - Igarashi, Atsushi

PB - Association for Computing Machinery, Inc

ER -