On Higher-Order Reachability Games Vs May Reachability

被引：1
作者：
Asada, Kazuyuki [1 ]
Katsura, Hiroyuki [2 ]
Kobayashi, Naoki [2 ]
机构：
[1] Tohoku Univ, Sendai, Miyagi, Japan
[2] Univ Tokyo, Tokyo, Japan
来源：
REACHABILITY PROBLEMS, RP 2022 | 2022年 / 13608卷
关键词：
MODEL CHECKING;
D O I：
10.1007/978-3-031-19135-0_8
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We consider the reachability problem for higher-order functional programs and study the relationship between reachability games (i.e., the reachability problem for programs with angelic and demonic nondeterminism) and may-reachability (i.e., the reachability problem for programs with only angelic nondeterminism). We show that reachability games for order-n programs can be reduced to may-reachability problems for order-(n + 1) programs, and vice versa. We formalize the reductions by using higher-order fixpoint logic and prove their correctness. We also discuss applications to higher-order program verification.
引用
收藏
页码：108 / 124
页数：17
相关论文
共 24 条
  • [1] Asada K., 2016, LIPICS, V55, DOI [10. 4230/LIPIcs.ICALP.2016.111, DOI 10.4230/LIPICS.ICALP.2016.111]
  • [2] Asada K., 2020, LIPICS, V167
  • [3] Asada K, 2024, Arxiv, DOI [arXiv:2203.08416, 10.48550/arXiv.2203.08416, DOI 10.48550/ARXIV.2203.08416]
  • [4] Higher-Order Constrained Horn Clauses for Verification
    Burn, Toby Cathcart
    Ong, C-H Luke
    Ramsay, Steven J.
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2018, 2
  • [5] ICE-Based Refinement Type Discovery for Higher-Order Functional Programs
    Champion, Adrien
    Chiba, Tomoya
    Kobayashi, Naoki
    Sato, Ryosuke
    [J]. JOURNAL OF AUTOMATED REASONING, 2020, 64 (07) : 1393 - 1418
  • [6] HoIce: An ICE-Based Non-linear Horn Clause Solver
    Champion, Adrien
    Kobayashi, Naoki
    Sato, Ryosuke
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2018, 2018, 11275 : 146 - 156
  • [7] FUNDAMENTAL-STUDIES - THE IO-HIERARCHIES AND OI-HIERARCHIES
    DAMM, W
    [J]. THEORETICAL COMPUTER SCIENCE, 1982, 20 (02) : 95 - 207
  • [8] Gradel E, 2002, LECT NOTES COMPUTER, V2500, DOI DOI 10.1007/3-540-36387-4
  • [9] Hojjat H, 2018, PROCEEDINGS OF THE 2018 18TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD), P158
  • [10] Predicate Abstraction and CEGAR for νHFLZ Validity Checking
    Iwayama, Naoki
    Kobayashi, Naoki
    Suzuki, Ryota
    Tsukada, Takeshi
    [J]. STATIC ANALYSIS (SAS 2020), 2020, 12389 : 134 - 155
123