TY - GEN
T1 - Combining higher-order model checking with refinement type inference
AU - Sato, Ryosuke
AU - Iwayama, Naoki
AU - Kobayashi, Naoki
N1 - Funding Information:
We would like to thank anonymous referees for useful comments. This work was supported by JSPS KAKENHI Grant Number JP15H05706 and JP18K18030.
Publisher Copyright:
© 2019 Association for Computing Machinery.
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
T2 - 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
Y2 - 14 January 2019 through 15 January 2019
ER -