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 条
  • [1] Model Checking Higher-Order Programs
    Kobayashi, Naoki
    JOURNAL OF THE ACM, 2013, 60 (03)
  • [2] 10 Years of the Higher-Order Model Checking Project
    Kobayashi, Naoki
    PROCEEDINGS OF THE 21ST INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING (PPDP 2019), 2019,
  • [3] On Model-Checking Higher-Order Effectful Programs
    Dal Lago, Ugo
    Ghyselen, Alexis
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2024, 8 (POPL):
  • [4] Model-Checking Higher-Order Functions
    Kobayashi, Naoki
    PPDP'09: PROCEEDINGS OF THE 11TH INTERNATIONAL ACM SIGPLAN SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING, 2009, : 25 - 36
  • [5] The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems
    Hague, Matthew
    To, Anthony Widjaja
    IARCS ANNUAL CONFERENCE ON FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE (FSTTCS 2010), 2010, 8 : 228 - 239
  • [6] Finitary Semantics of Linear Logic and Higher-Order Model-Checking
    Grellois, Charles
    Mellies, Paul-Andre
    MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2015, PT I, 2015, 9234 : 256 - 268
  • [7] Exact Flow Analysis by Higher-Order Model Checking
    Tobita, Yoshihiro
    Tsukada, Takeshi
    Kobayashi, Naoki
    FUNCTIONAL AND LOGIC PROGRAMMING (FLOPS 2012), 2012, 7294 : 275 - 289
  • [8] A Traversal-based Algorithm for Higher-Order Model Checking
    Neatherway, Robin P.
    Ong, C. -H. Luke
    Ramsay, Steven J.
    ACM SIGPLAN NOTICES, 2012, 47 (09) : 353 - 364
  • [9] A Type-Directed Abstraction Refinement Approach to Higher-Order Model Checking
    Ramsay, Steven J.
    Neatherway, Robin P.
    Ong, C. -H. Luke
    ACM SIGPLAN NOTICES, 2014, 49 (01) : 61 - 72
  • [10] Space-Efficient Model-Checking of Higher-Order Recursion Schemes
    Bruse, Florian
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2025, PT I, 2025, 15529 : 29 - 51
1234