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 条
  • [21] On the Termination Problem for Probabilistic Higher-Order Recursive Programs
    Kobayashi, Naoki
    Dal Lago, Ugo
    Grellois, Charles
    [J]. 2019 34TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2019,
  • [22] ON THE TERMINATION PROBLEM FOR PROBABILISTIC HIGHER-ORDER RECURSIVE PROGRAMS
    Kobayashi, Naoki
    Dal Lago, Ugo
    Grellois, Charles
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2020, 16 (04) : 1 - 57
  • [23] Towards a logic programming methodology based on higher-order predicates
    Hamfelt, A
    Nilsson, JF
    [J]. NEW GENERATION COMPUTING, 1997, 15 (04) : 421 - 447
  • [24] Towards a logic programming methodology based on higher-order predicates
    Andreas Hamfelt
    Jørgen Fischer Nilsson
    [J]. New Generation Computing, 1997, 15 : 421 - 447
  • [25] Wavelets' filters and higher-order frequency analysis of acoustic emission signals from termite activity
    Gonzalez-de-la-Rosa, Juan-Jose
    Aguera-Perez, Agustin
    Palomares-Salas, Jose-Carlos
    Sierra-Fernandez, Jose-Maria
    [J]. MEASUREMENT, 2016, 93 : 315 - 318
  • [26] Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties
    Broadbent, Christopher H.
    Carayol, Arnaud
    Ong, C-H Luke
    Serre, Olivier
    [J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2021, 22 (02)
  • [27] C-SHORe A Collapsible Approach to Verifying Higher-Order Programs
    Broadbent, Christopher
    Carayol, Arnaud
    Hague, Matthew
    Serre, Olivier
    [J]. ACM SIGPLAN NOTICES, 2013, 48 (09) : 13 - 24
  • [28] Higher-Order Averaging, Formal Series and Numerical Integration I: B-series
    Chartier, P.
    Murua, A.
    Sanz-Serna, J. M.
    [J]. FOUNDATIONS OF COMPUTATIONAL MATHEMATICS, 2010, 10 (06) : 695 - 727
  • [29] Higher-Order Averaging, Formal Series and Numerical Integration I: B-series
    P. Chartier
    A. Murua
    J. M. Sanz-Serna
    [J]. Foundations of Computational Mathematics, 2010, 10 : 695 - 727
  • [30] Higher-Order Averaging, Formal Series and Numerical Integration II: The Quasi-Periodic Case
    Chartier, P.
    Murua, A.
    Sanz-Serna, J. M.
    [J]. FOUNDATIONS OF COMPUTATIONAL MATHEMATICS, 2012, 12 (04) : 471 - 508
1234