Naoki Kobayashi

ORCID

Publication Activity (10 Years)

Years Active: 1992-2024
Publications (10 Years): 88

Top Venues

Publications

Mahmudul Faisal Al Ameen, Naoki Kobayashi, Ryosuke Sato
Asynchronous unfold/fold transformation for fixpoint logic. Sci. Comput. Program. 231 (2024)
Takashi Nakayama, Yusuke Matsushita, Ken Sakayori, Ryosuke Sato, Naoki Kobayashi
Borrowable Fractional Ownership Types for Verification. VMCAI (2) (2024)
Izumi Tanaka, Ken Sakayori, Naoki Kobayashi
Ownership Types for Verification of Programs with Pointer Arithmetic. CoRR (2023)
Takashi Nakayama, Yusuke Matsushita, Ken Sakayori, Ryosuke Sato, Naoki Kobayashi
Borrowable Fractional Ownership Types for Verification. CoRR (2023)
Hiroyuki Katsura, Naoki Kobayashi, Ryosuke Sato
Higher-Order Property-Directed Reachability. Proc. ACM Program. Lang. 7 (ICFP) (2023)
Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, Takeshi Tsukada
HFL(Z) Validity Checking for Automated Program Verification. Proc. ACM Program. Lang. 7 (POPL) (2023)
Ryo Ikeda, Ryosuke Sato, Naoki Kobayashi
Argument Reduction of Constrained Horn Clauses Using Equality Constraints. APLAS (2023)
Momoko Hattori, Naoki Kobayashi, Ryosuke Sato
Gradual Tensor Shape Checking. ESOP (2023)
Naoki Kobayashi, Minchao Wu
Neural Network-Guided Synthesis of Recursive List Functions. TACAS (1) (2023)
Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi
On Higher-Order Reachability Games vs May Reachability. CoRR (2022)
Momoko Hattori, Naoki Kobayashi, Ryosuke Sato
Gradual Tensor Shape Checking. CoRR (2022)
Mahmudul Faisal Al Ameen, Naoki Kobayashi, Ryosuke Sato
Asynchronous Unfold/Fold Transformation for Fixpoint Logic. FLOPS (2022)
Ryoya Mukai, Naoki Kobayashi, Ryosuke Sato
Parameterized Recursive Refinement Types for Automated Program Verification. SAS (2022)
Kento Tanahashi, Naoki Kobayashi, Ryosuke Sato
Automatic HFL(Z) Validity Checking for Program Verification. CoRR (2022)
Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi
On Higher-Order Reachability Games Vs May Reachability. RP (2022)
Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno
Toward Neural-Network-Guided Program Synthesis and Verification. SAS (2021)
Yo Mitani, Naoki Kobayashi, Takeshi Tsukada
A Probabilistic Higher-order Fixpoint Logic. Log. Methods Comput. Sci. 17 (4) (2021)
Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada
Termination Analysis for the π-Calculus by Reduction to Sequential Program Termination. CoRR (2021)
Hideto Ueno, John Toman, Naoki Kobayashi, Takeshi Tsukada
Counterexample generation for program verification based on ownership refinement types. PEPM@POPL (2021)
Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
RustHorn: CHC-based Verification for Rust Programs. ACM Trans. Program. Lang. Syst. 43 (4) (2021)
Patrick Baillot, Alexis Ghyselen, Naoki Kobayashi
Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes. CONCUR (2021)
Patrick Baillot, Alexis Ghyselen, Naoki Kobayashi
Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes. CoRR (2021)
Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno
Toward Neural-Network-Guided Program Synthesis and Verification. CoRR (2021)
Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving. SAS (2021)
Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi
A Cyclic Proof System for HFL_ℕ. CSL (2021)
Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada
Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination. APLAS (2021)
Ryuta Kambe, Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, Ryo Yoshinaka
Inside-Outside Algorithm for Macro Grammars. ICGI (2021)
Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving. CoRR (2021)
Yo Mitani, Naoki Kobayashi, Takeshi Tsukada
A Probabilistic Higher-order Fixpoint Logic. CoRR (2020)
Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato
ICE-Based Refinement Type Discovery for Higher-Order Functional Programs. J. Autom. Reason. 64 (7) (2020)
Yo Mitani, Naoki Kobayashi, Takeshi Tsukada
A Probabilistic Higher-Order Fixpoint Logic. FSCD (2020)
Naoki Kobayashi, Ugo Dal Lago, Charles Grellois
On the Termination Problem for Probabilistic Higher-Order Recursive Programs. Log. Methods Comput. Sci. 16 (4) (2020)
Hiroyuki Katsura, Naoki Iwayama, Naoki Kobayashi, Takeshi Tsukada
A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking. APLAS (2020)
Hiroaki Naganuma, Diptarama Hendrian, Ryo Yoshinaka, Ayumi Shinohara, Naoki Kobayashi
Grammar compression with probabilistic context-free grammar. CoRR (2020)
Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi
A Cyclic Proof System for HFLN. CoRR (2020)
Naoki Iwayama, Naoki Kobayashi, Ryota Suzuki, Takeshi Tsukada
Predicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking. SAS (2020)
Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
RustHorn: CHC-based Verification for Rust Programs (full version). CoRR (2020)
Naoki Kobayashi, Grigory Fedyukovich, Aarti Gupta
Fold/Unfold Transformations for Fixpoint Logic. TACAS (2) (2020)
John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs. ESOP (2020)
Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
RustHorn: CHC-Based Verification for Rust Programs. ESOP (2020)
Hiroaki Naganuma, Diptarama Hendrian, Ryo Yoshinaka, Ayumi Shinohara, Naoki Kobayashi
Grammar Compression with Probabilistic Context-Free Grammar. DCC (2020)
Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada
On Average-Case Hardness of Higher-Order Model Checking. FSCD (2020)
Kazuyuki Asada, Naoki Kobayashi
Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars. FSCD (2020)
John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs. CoRR (2020)
Keiichi Watanabe, Takeshi Tsukada, Hiroki Oshikawa, Naoki Kobayashi
Reduction from branching-time property verification of higher-order programs to HFL validity checking. PEPM@POPL (2019)
Naoki Kobayashi
Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable. Theor. Comput. Sci. 777 (2019)
Naoki Kobayashi, Ugo Dal Lago, Charles Grellois
On the Termination Problem for Probabilistic Higher-Order Recursive Programs. LICS (2019)
Naoki Kobayashi
10 Years of the Higher-Order Model Checking Project (Extended Abstract). PPDP (2019)
Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence. Log. Methods Comput. Sci. 15 (1) (2019)
Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada
A Type-Based HFL Model Checking Algorithm. CoRR (2019)
Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada
A Type-Based HFL Model Checking Algorithm. APLAS (2019)
Ryosuke Sato, Naoki Iwayama, Naoki Kobayashi
Combining higher-order model checking with refinement type inference. PEPM@POPL (2019)
Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, Hiroshi Unno
Temporal Verification of Programs via First-Order Fixpoint Logic. SAS (2019)
Yuya Okuyama, Takeshi Tsukada, Naoki Kobayashi
A Temporal Logic for Higher-Order Functional Programs. SAS (2019)
Adrien Champion, Naoki Kobayashi, Ryosuke Sato
HoIce: An ICE-Based Non-linear Horn Clause Solver. APLAS (2018)
Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe
Higher-Order Program Verification via HFL Model Checking. ESOP (2018)
Shingo Eguchi, Naoki Kobayashi, Takeshi Tsukada
Automated Synthesis of Functional Programs with Auxiliary Functions. APLAS (2018)
Naoki Kobayashi, Ugo Dal Lago, Charles Grellois
On the Termination Problem for Probabilistic Higher-Order Recursive Programs. CoRR (2018)
Kazuyuki Asada, Naoki Kobayashi
Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered. FSTTCS (2018)
Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence. CoRR (2018)
Magnús M. Halldórsson, Naoki Kobayashi, Bettina Speckmann
Special issue for the 42nd International Colloquium on Automata, Languages and Programming, ICALP 2015, Kyoto, Japan. Inf. Comput. 261 (2018)
Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato
ICE-Based Refinement Type Discovery for Higher-Order Functional Programs. TACAS (1) (2018)
Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi, Atsushi Igarashi
Verification of code generators via higher-order model checking. PEPM (2017)
Kazuyuki Asada, Naoki Kobayashi
Pumping Lemma for Higher-order Languages. ICALP (2017)
Ryosuke Sato, Naoki Kobayashi
Modular Verification of Higher-Order Functional Programs. ESOP (2017)
Ryoma Sin'ya, Kazuyuki Asada, Naoki Kobayashi, Takeshi Tsukada
Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence. FoSSaCS (2017)
Naoki Kobayashi, Étienne Lozes, Florian Bruse
On the relationship between higher-order recursion schemes and higher-order fixpoint logic. POPL (2017)
Kazuyuki Asada, Naoki Kobayashi
Pumping Lemma for Higher-order Languages. CoRR (2017)
Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi
Verifying relational properties of functional programs by first-order refinement. Sci. Comput. Program. 137 (2017)
Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, Takeshi Tsukada
Streett Automata Model Checking of Higher-Order Recursion Schemes. FSCD (2017)
Naoki Kobayashi, Cosimo Laneve
Deadlock analysis of unbounded process networks. Inf. Comput. 252 (2017)
Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe
Higher-Order Program Verification via HFL Model Checking. CoRR (2017)
Kotaro Takeda, Naoki Kobayashi, Kazuya Yaguchi, Ayumi Shinohara
Compact bit encoding schemes for simply-typed lambda-terms. ICFP (2016)
Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi
Automatically disproving fair termination of higher-order functional programs. ICFP (2016)
Naoki Kobayashi, Luke Ong, Igor Walukiewicz
Higher-Order Model Checking (NII Shonan Meeting 2016-4). NII Shonan Meet. Rep. 2016 (2016)
Xin Li, Naoki Kobayashi
Equivalence-Based Abstraction Refinement for \mu HORS Model Checking. ATVA (2016)
Taku Terao, Takeshi Tsukada, Naoki Kobayashi
Higher-Order Model Checking in Direct Style. APLAS (2016)
Kazuhide Yasukata, Takeshi Tsukada, Naoki Kobayashi
Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation. APLAS (2016)
Kazuyuki Asada, Naoki Kobayashi
On Word and Frontier Languages of Unsafe Higher-Order Grammars. ICALP (2016)
Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno
Temporal verification of higher-order functional programs. POPL (2016)
Kazuyuki Asada, Naoki Kobayashi
On Word and Frontier Languages of Unsafe Higher-Order Grammars. CoRR (2016)
Sadaaki Kawata, Kazuyuki Asada, Naoki Kobayashi
Decision Algorithms for Checking Definability of Order-2 Finitary PCF. APLAS (2015)
Naoki Kobayashi, Xin Li
Automata-Based Abstraction Refinement for µHORS Model Checking. LICS (2015)
Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs. CAV (2) (2015)
Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
Verification of tree-processing programs via higher-order mode checking. Math. Struct. Comput. Sci. 25 (4) (2015)
Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi
Verifying Relational Properties of Functional Programs by First-Order Refinement. PEPM (2015)
Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi
Refinement Type Checking via Assertion Checking. J. Inf. Process. 23 (6) (2015)
Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno
Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs. APLAS (2015)
Taku Terao, Naoki Kobayashi
A ZDD-Based Efficient Higher-Order Model Checking Algorithm. APLAS (2014)
Naoki Kobayashi
From Linear Types to Behavioural Types and Model Checking. Concurrent Objects and Beyond (2014)
Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi
Automatic Termination Verification for Higher-Order Functional Programs. ESOP (2014)
Elena Giachino, Naoki Kobayashi, Cosimo Laneve
Deadlock Analysis of Unbounded Process Networks. CONCUR (2014)
Takeshi Tsukada, Naoki Kobayashi
Complexity of Model-Checking Call-by-Value Programs. FoSSaCS (2014)
Kazuya Yaguchi, Naoki Kobayashi, Ayumi Shinohara
Efficient Algorithm and Coding for Higher-Order Compression. DCC (2014)
Kazuhide Yasukata, Naoki Kobayashi, Kazutaka Matsuda
Pairwise Reachability Analysis for Higher Order Concurrent Programs by Higher-Order Model Checking. CONCUR (2014)
Naoki Kobayashi, Kazuhiro Inaba, Takeshi Tsukada
Unsafe Order-2 Tree Languages Are Context-Sensitive. FoSSaCS (2014)
Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
Automating relatively complete verification of higher-order functional programs. POPL (2013)
Naoki Kobayashi, Atsushi Igarashi
Model-Checking Higher-Order Programs with Recursive Types. ESOP (2013)
Naoki Kobayashi
Model Checking Higher-Order Programs. J. ACM 60 (3) (2013)
Koichi Fujima, Sohei Ito, Naoki Kobayashi
Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes. APLAS (2013)

Naoki Kobayashi.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Naoki Kobayashi