Automating Relatively Complete Verification of Higher-Order Functional Programs

被引：27
|
作者：
Unno, Hiroshi [1 ]
Terauchi, Tachio [2 ]
Kobayashi, Naoki [3 ]
机构：
[1] Univ Tsukuba, Tsukuba, Ibaraki 305, Japan
[2] Nagoya Univ, Nagoya, Aichi 4648601, Japan
[3] Univ Tokyo, Tokyo 1138654, Japan
来源：
ACM SIGPLAN NOTICES | 2013年 / 48卷 / 01期
关键词：
Relative Completeness; Higher-Order Programs; Software Model Checking; Type Inference; LANGUAGE;
D O I：
10.1145/2480359.2429081
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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.
引用
收藏
页码：75 / 86
页数：12
相关论文
共 50 条
  • [41] Termination Analysis and Call Graph Construction for Higher-Order Functional Programs
    Sereni, Damien
    [J]. ICFP'07 PROCEEDINGS OF THE 2007 ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING, 2007, : 71 - 83
  • [42] Termination analysis and call graph construction for higher-order functional programs
    Sereni, Damien
    [J]. ACM SIGPLAN NOTICES, 2007, 42 (09) : 71 - 83
  • [43] Relational semantics for higher-order programs
    Aboul-Hosn, Kamal
    Kozen, Dexter
    [J]. MATHEMATICS OF PROGRAM CONSTRUCTION, 2006, 4014 : 29 - 48
  • [44] Learning higher-order logic programs
    Cropper, Andrew
    Morel, Rolf
    Muggleton, Stephen
    [J]. MACHINE LEARNING, 2020, 109 (07) : 1289 - 1322
  • [45] Model Checking Higher-Order Programs
    Kobayashi, Naoki
    [J]. JOURNAL OF THE ACM, 2013, 60 (03)
  • [46] Learning higher-order logic programs
    Andrew Cropper
    Rolf Morel
    Stephen Muggleton
    [J]. Machine Learning, 2020, 109 : 1289 - 1322
  • [47] MACHINE LEARNING OF HIGHER-ORDER PROGRAMS
    BALIGA, G
    CASE, J
    JAIN, S
    SURAJ, M
    [J]. JOURNAL OF SYMBOLIC LOGIC, 1994, 59 (02) : 486 - 500
  • [48] Higher-order transformation of logic programs
    Seres, S
    Spivey, M
    [J]. LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 2001, 2042 : 57 - 68
  • [49] MACHINE LEARNING OF HIGHER-ORDER PROGRAMS
    BALIGA, G
    CASE, J
    JAIN, S
    SURAJ, M
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 620 : 9 - 20
  • [50] Refinement of higher-order logic programs
    Colvin, R
    Hayes, I
    Hemer, D
    Strooper, P
    [J]. LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 2003, 2664 : 126 - 143
12345