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 条
  • [1] Relatively Complete Counterexamples for Higher-Order Programs
    Nguyen, Phuc C.
    Van Horn, David
    [J]. ACM SIGPLAN NOTICES, 2015, 50 (06) : 446 - 456
  • [2] Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs
    Unno, Hiroshi
    Satake, Yuki
    Terauchi, Tachio
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2018, 2
  • [3] Modular Verification of Higher-Order Functional Programs
    Sato, Ryosuke
    Kobayashi, Naoki
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS (ESOP 2017): 26TH EUROPEAN SYMPOSIUM ON PROGRAMMING, 2017, 10201 : 831 - 854
  • [4] Temporal Verification of Higher-Order Functional Programs
    Murase, Akihiro
    Terauchi, Tachio
    Kobayashi, Naoki
    Sato, Ryosuke
    Unno, Hiroshi
    [J]. ACM SIGPLAN NOTICES, 2016, 51 (01) : 57 - 68
  • [5] Automated Verification of Higher-Order Functional Programs
    Terauchi, Tachio
    [J]. FUNCTIONAL AND LOGIC PROGRAMMING (FLOPS 2012), 2012, 7294 : 2 - 2
  • [6] Automatic Termination Verification for Higher-Order Functional Programs
    Kuwahara, Takuya
    Terauchi, Tachio
    Unno, Hiroshi
    Kobayashi, Naoki
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, 2014, 8410 : 392 - 411
  • [7] VERIFICATION OF PROGRAMS WITH HIGHER-ORDER ARRAYS
    KOWALCZYK, W
    URZYCZYN, P
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1987, 278 : 251 - 258
  • [8] Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs
    Kobayashi, Naoki
    [J]. ACM SIGPLAN NOTICES, 2009, 44 (01) : 416 - 428
  • [9] Formal Verification of Higher-Order Probabilistic Programs
    Sato, Tetsuya
    Aguirre, Alejandro
    Barthe, Gilles
    Gaboardi, Marco
    Garg, Deepak
    Hsu, Justin
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (POPL):
  • [10] SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References
    Jaber, Guilhem
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4
12345