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
AN - SCOPUS:84874181407
SN - 9781450318327
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 75
EP - 86
BT - POPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
T2 - 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013
Y2 - 23 January 2013 through 25 January 2013
ER -