Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 711 2018 [Refereed]

ICE-Based Refinement Type Discovery for Higher-Order Functional Programs

Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato

Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thes 365 2018 [Refereed]

Deadlock analysis of unbounded process networks

Naoki Kobayashi, Cosimo Laneve

Inf. Comput. 252 48 2017 [Refereed]

Almost Every Simply Typed \(λ\)-Term Has a Long \(β\)-Reduction Sequence

Ryoma Sin'ya, Kazuyuki Asada, Naoki Kobayashi, Takeshi Tsukada

Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, 53 2017 [Refereed]

Pumping Lemma for Higher-order Languages

Kazuyuki Asada, Naoki Kobayashi

44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland 97:1 2017 [Refereed]

Modular Verification of Higher-Order Functional Programs

Ryosuke Sato, Naoki Kobayashi

Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 831 2017 [Refereed]

On the relationship between higher-order recursion schemes and higher-order fixpoint logic

Naoki Kobayashi, {É}tienne Lozes, Florian Bruse

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 246 2017 [Refereed]

Streett Automata Model Checking of Higher-Order Recursion Schemes

Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, Takeshi Tsukada

2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK 32:1 2017 [Refereed]

Verifying relational properties of functional programs by first-order refinement

Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi

Sci. Comput. Program. 137 2 2017 [Refereed]

Verification of code generators via higher-order model checking

Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi, Atsushi Igarashi

Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2017, Paris, France, January 18-20, 2017 59 2017 [Refereed]

On Word and Frontier Languages of Unsafe Higher-Order Grammars

Kazuyuki Asada, Naoki Kobayashi

43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy 111:1 2016 [Refereed]

Compact bit encoding schemes for simply-typed lambda-terms

Kotaro Takeda, Naoki Kobayashi, Kazuya Yaguchi, Ayumi Shinohara

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016 146 2016 [Refereed]

Higher-Order Model Checking in Direct Style

Taku Terao, Takeshi Tsukada, Naoki Kobayashi

Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings 295 2016 [Refereed]

Automatically disproving fair termination of higher-order functional programs

Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016 243 2016 [Refereed]

Equivalence-Based Abstraction Refinement for \mu HORS Model Checking

Xin Li, Naoki Kobayashi

Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings 304 2016 [Refereed]

Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation

Kazuhide Yasukata, Takeshi Tsukada, Naoki Kobayashi

Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings 335 2016 [Refereed]

Temporal verification of higher-order functional programs

Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016 57 2016 [Refereed]

Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs

Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno

Programming Languages and Systems - 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings 295 2015 [Refereed]

Automata-Based Abstraction Refinement for \(µ\)HORS Model Checking

Naoki Kobayashi, Xin Li

30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015 713 2015 [Refereed]

Refinement Type Checking via Assertion Checking

Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi

JIP 23(6) 827 2015 [Refereed]

Verification of tree-processing programs via higher-order mode checking

Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi

Mathematical Structures in Computer Science 25(4) 841 2015 [Refereed]

Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs

Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi

Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II 287 2015 [Refereed]

Decision Algorithms for Checking Definability of Order-2 Finitary PCF

Sadaaki Kawata, Kazuyuki Asada, Naoki Kobayashi

Programming Languages and Systems - 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings 313 2015 [Refereed]

Verifying Relational Properties of Functional Programs by First-Order Refinement

Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi

Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM, Mumbai, India, January 15-17, 2015 61 2015 [Refereed]

Automatic Termination Verification for Higher-Order Functional Programs

Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi

Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 392 2014 [Refereed]

A ZDD-Based Efficient Higher-Order Model Checking Algorithm

Taku Terao, Naoki Kobayashi

Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings 354 2014 [Refereed]

From Linear Types to Behavioural Types and Model Checking

Naoki Kobayashi

Concurrent Objects and Beyond - Papers dedicated to Akinori Yonezawa on the Occasion of His 65th Birthday 128 2014 [Refereed]

Efficient Algorithm and Coding for Higher-Order Compression

Kazuya Yaguchi, Naoki Kobayashi, Ayumi Shinohara

Data Compression Conference, DCC 2014, Snowbird, UT, USA, 26-28 March, 2014 434 2014 [Refereed]

Unsafe Order-2 Tree Languages Are Context-Sensitive

Naoki Kobayashi, Kazuhiro Inaba, Takeshi Tsukada

Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, 149 2014 [Refereed]

Deadlock Analysis of Unbounded Process Networks

Elena Giachino, Naoki Kobayashi, Cosimo Laneve

CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings 63 2014 [Refereed]

Complexity of Model-Checking Call-by-Value Programs

Takeshi Tsukada, Naoki Kobayashi

Pairwise Reachability Analysis for Higher Order Concurrent Programs by Higher-Order Model Checking

Kazuhide Yasukata, Naoki Kobayashi, Kazutaka Matsuda

CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings 312 2014 [Refereed]

Automating relatively complete verification of higher-order functional programs

Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi

The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013 75 2013 [Refereed]

Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes

Koichi Fujima, Sohei Ito, Naoki Kobayashi

Programming Languages and Systems - 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013. Proceedings 17 2013 [Refereed]

Model Checking Higher-Order Programs

Naoki Kobayashi

J. ACM 60(3) 20:1 2013 [Refereed]

Pumping by Typing

Naoki Kobayashi

28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013 398 2013 [Refereed]

Saturation-Based Model Checking of Higher-Order Recursion Schemes

Christopher H. Broadbent, Naoki Kobayashi

Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy 129 2013 [Refereed]

Model-Checking Higher-Order Programs with Recursive Types

Naoki Kobayashi, Atsushi Igarashi

Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 20 431 2013 [Refereed]

Towards a scalable software model checker for higher-order programs

Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi

Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013, Rome, Italy, January 21-22, 2013 53 2013 [Refereed]

Conference Activities & Talks

Plain Text

10 Years of the Higher-Order Model Checking Project [Invited]

Naoki Kobayashi

21st International Symposium on Principles and Practice of Programming Languages (PPDP 2019) 9 Oct 2019

On Two Kinds of Higher-Order Model Checking and Higher-Order Program Verification [Invited]

Naoki Kobayashi

HOR 2018 2018

On Two Higher-Order Extensions of Model Checking [Invited]

Naoki Kobayashi

FTSCS 2016 2016

Program Certification by Higher-Order Model Checking [Invited]

Naoki Kobayashi

CPP 2012 2012

Towards a software model checker for ML [Invited]

Naoki Kobayashi

ML Workshop 2011

Higher-Order Program Verification and Language-Based Security [Invited]

Naoki Kobayashi

ASIAN 2009 2009

Types and Recursion Schemes for Higher-Order Program Verification [Invited]

Naoki Kobayashi

APLAS 2009 2009

Substructural Type Systems for Program Analysis [Invited]

Naoki Kobayashi

FLOPS 2008 2008

Higher-Order Model Checking: From Theory to Practice [Invited]

Naoki Kobayashi

LICS 2011 2011

Type Systems for Concurrent Processes: From Deadlock-Freedom to Livelock-Freedom, Time-Boundedness [Invited]

Naoki Kobayashi

IFIP TCS 2000 2000