10 Years of the Higher-Order Model Checking Project

被引：2
|
作者：
Kobayashi, Naoki [1 ]
机构：
[1] Univ Tokyo, Tokyo, Japan
来源：
PROCEEDINGS OF THE 21ST INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING (PPDP 2019) | 2019年
关键词：
higher-order model checking; program verification; RECURSION SCHEMES; VERIFICATION; TERMINATION; TREES;
D O I：
10.1145/3354166.3354167
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We give an overview of the higher-order model checking project at the University of Tokyo. We provide references to the results obtained in the past 10 years, and explain what the project is now heading for.
引用
收藏
页数：2
相关论文
共 50 条
  • [1] Higher-Order Model Checking
    Ong, C. -H. Luke
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (77): : 13 - 13
  • [2] Model Checking Higher-Order Programs
    Kobayashi, Naoki
    [J]. JOURNAL OF THE ACM, 2013, 60 (03)
  • [3] Higher-Order Model Checking: An Overview
    Ong, Luke
    [J]. 2015 30TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2015, : 1 - 15
  • [4] Higher-Order Model Checking in Direct Style
    Terao, Taku
    Tsukada, Takeshi
    Kobayashi, Naoki
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2016, 2016, 10017 : 295 - 313
  • [5] Model-Checking Higher-Order Functions
    Kobayashi, Naoki
    [J]. PPDP'09: PROCEEDINGS OF THE 11TH INTERNATIONAL ACM SIGPLAN SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING, 2009, : 25 - 36
  • [6] THE COMPLEXITY OF MODEL CHECKING HIGHER-ORDER FIXPOINT LOGIC
    Axelsson, Roland
    Lange, Martin
    Somla, Rafal
    [J]. Logical Methods in Computer Science, 2007, 3 (02)
  • [7] Predicate Abstraction and CEGAR for Higher-Order Model Checking
    Kobayashi, Naoki
    Sato, Ryosuke
    Unno, Hiroshi
    [J]. ACM SIGPLAN NOTICES, 2011, 46 (06) : 222 - 233
  • [8] Higher-Order Model Checking: From Theory to Practice
    Kobayashi, Naoki
    [J]. 26TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2011), 2011, : 219 - 224
  • [9] Indexed linear logic and higher-order model checking
    Grellois, Charles
    Mellies, Paul-Andre
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (177): : 43 - 52
  • [10] On Model-Checking Higher-Order Effectful Programs
    Dal Lago, Ugo
    Ghyselen, Alexis
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2024, 8 (POPL):
12345