Higher-Order Model Checking: From Theory to Practice

被引：3
|
作者：
Kobayashi, Naoki [1 ]
机构：
[1] Tohoku Univ, Sendai, Miyagi 980, Japan
来源：
26TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2011) | 2011年
关键词：
RECURSION SCHEMES; LEVEL-2; TREES;
D O I：
10.1109/LICS.2011.15
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
The model checking of higher-order recursion schemes (higher-order model checking for short) has been actively studied in the last decade, and has seen significant progress in both theory and practice. From a practical perspective, higher-order model checking provides a foundation for software model checkers for functional programming languages such as ML and Haskell. This short article aims to provide an overview of the recent progress in higher-order model checking and discuss future directions.
引用
收藏
页码：219 / 224
页数：6
相关论文
共 34 条
  • [11] Verification of tree-processing programs via higher-order mode checking
    Unno, Hiroshi
    Tabuchi, Naoshi
    Kobayashi, Naoki
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2015, 25 (04) : 841 - 866
  • [12] Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking
    Watanabe, Keiichi
    Tsukada, Takeshi
    Oshikawa, Hiroki
    Kobayashi, Naoki
    PROCEEDINGS OF THE 2019 ACM SIGPLAN WORKSHOP ON PARTIAL EVALUATION AND PROGRAM MANIPULATION (PEPM '19), 2019, : 22 - 34
  • [13] Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs
    Kobayashi, Naoki
    ACM SIGPLAN NOTICES, 2009, 44 (01) : 416 - 428
  • [14] Krivine machines and higher-order schemes
    Salvati, Sylvain
    Walukiewicz, Igor
    INFORMATION AND COMPUTATION, 2014, 239 : 340 - 355
  • [15] On the Relationship between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic
    Kobayashi, Naoki
    Lozes, Etienne
    Bruse, Florian
    ACM SIGPLAN NOTICES, 2017, 52 (01) : 246 - 259
  • [16] Krivine Machines and Higher-Order Schemes
    Salvati, S.
    Walukiewicz, I.
    AUTOMATA, LANGUAGES AND PROGRAMMING, ICALP, PT II, 2011, 6756 : 162 - 173
  • [17] Linearity in Higher-Order Recursion Schemes
    Clairambault, Pierre
    Grellois, Charles
    Murawski, Andrzej S.
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2018, 2
  • [18] Models of Higher-Order Computation: Recursion Schemes and Collapsible Pushdown Automata
    Ong, C. -H. L.
    LOGICS AND LANGUAGES FOR RELIABILITY AND SECURITY, 2010, 25 : 263 - 299
  • [19] Higher-Order Property-Directed Reachability
    Katsura, Hiroyuki
    Kobayashi, Naoki
    Sato, Ryosuke
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2023, 7 (ICFP):
  • [20] On the Termination Problem for Probabilistic Higher-Order Recursive Programs
    Kobayashi, Naoki
    Dal Lago, Ugo
    Grellois, Charles
    2019 34TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2019,
1234