小林直樹 Kobayashi Naoki

研究者番号	00262155
その他のID
所属 (現在)	2026年度: 東京大学, 大学院情報理工学系研究科, 教授
所属 (過去の研究課題情報に基づく) *注記	2026年度: 東京大学, 大学院情報理工学系研究科, 教授 2015年度 – 2024年度: 東京大学, 大学院情報理工学系研究科, 教授 2016年度: 東京大学, 情報理工学系研究科, 教授 2012年度 – 2015年度: 東京大学, 情報理工学(系)研究科, 教授 2011年度: 東北大学, 情報科学研究科, 教授 … もっと見る 2007年度 – 2011年度: 東北大学, 大学院・情報科学研究科, 教授 2006年度: 東北大学, 大学院情報科学研究科, 教授 2004年度 – 2005年度: 東北大学, 大学院・情報科学研究科, 教授 2003年度: 東京工業大学, 工学部, 助教授 2003年度: 東京工業大学, 情報理工学研究科, 助教授 2000年度 – 2003年度: 東京工業大学, 大学院・情報理工学研究科, 助教授 2002年度: 東京工業大学, 大学院・情報理工学研究所, 助教授 2000年度: 東京大学, 大学院・理学研究科, 専任講師 1996年度 – 2000年度: 東京大学, 大学院・理学系研究科, 講師 1995年度: 東京大学, 大学院・理学系研究科, 助手 1994年度: 東京大学, 大学院理学系研究科, 助手隠す
審査区分/研究分野	研究代表者計算機科学 / 理工系 / 中区分60:情報科学、情報工学およびその関連分野 / 情報学基礎 / ソフトウエア / 大区分J / 情報学基礎理論研究代表者以外計算機科学 / ソフトウェア / ソフトウエア / 情報学基礎
キーワード	研究代表者型システム / プログラム検証 / 高階モデル検査 / プログラム解析 / デッドロック / 並行プログラミング言語 / 高階不動点論理 / 関数型プログラム / 型理論 / プログラム変換 … もっと見る / 情報流解析 / 資源使用法解析 / 並行プログラム / モデル検査 / 分散プログラミング言語 / 線形論理 / 不動点論理 / information flow analysis / program analysis / 型推論 / Java / 関数型言語 / 高階文法 / データ圧縮 / 高階再帰スキーム / XML / XML文書型 / バッファリング / ストリーム処理 / 木構造処理 / 順序付き線形型 / ソフトウェア検証 / Coq / 定理証明支援器 / リージョン推論 / メモリ管理 / 線形型 / プロセス計算 / 静的解析 / 並列言語 / 機械学習 / 確率付き高階不動点論理 / 共通型 / 高階論理 / 確率付き文法 / concurrent programs / functional programs / type theory / program verification / 双模倣 / 割り込み / 線形最適化問題 / プログラム等価性 / resource / static analysis of communication / proof assistant / safety / concurrent program / security / type system / ライブロック / 様相論理 / 計算資源 / 通信の解析 / 安全性 / セキュリティ / resource usage analysis / functional language / type inference / garbage collection / region inference / memory management / quasi-linear types / linear type system / 通信チャネル / 並行言語 / 並列計算機 / 資源使用解析 / ガベージコレクション / 擬似線形型 / 線形型システム / object-oriented programming / linear logic / process calculus / deadlock / type systems / concurrency / distributed programming / 部分評価 / オブジェクト指向 / ツリーオートマトン / メモリ使用法解析 / 述語抽象化 / 資源使用法検証 / 順序付非線形型 / 順序付線形型 / 構成的プログラミング / プログラム抽出 / リ-ジョン推論 / 並列オブジェクト指向 / 並列計算 … もっと見る研究代表者以外線形論理 / 並列言語 / 並列オブジェクト / 実時間システム / 形式検証 / 形式仕様 / Web Crawling / Concurrent objects / ABCL / 証明論 / 論理的手法 / 証明支援系 / 仕様記述・検証 / ソフトウェアの安全性 / 証明検証 / 型理論 / クラス理論 / proof theory / real-time system / formal verification / formal specification / linear logic / logical method / Real-Time System / Formal Specification / Formal Verifieation / Linear Logic / 定時間システム / Software Substrate / adaptive / Grid Computing / 動的コード生成 / プログラム特化 / ボトルネック / 性能予測 / 並列・分散ごみ集め / タスク配置 / 適応的計算 / 性能予測モデル / 並列GC / 並列メモリ管理 / 共有メモリ / 排他制御 / 自己組織化ネットワーク / 動的負荷分散 / 自動並列化 / 基盤ソフトウェア / 適応的 / Grid計算 / distributed GC / multithread / partial evaluation / deadlock / type systems / synchronous channels / concurrent objects / concurrent programming language / 並列プログラミング / 分散GC / マルチスレッド / 部分計算 / デッドロック / 型システム / 同期チャネル / 並列プログラミング言語 / Static analysis / Linear logic / Concurrent computation / 型推論 / 並列オブジェクト指向言語 / 並列計算 / 線型タイプ / 静的解析 / 並列オブジェクト指向 / 並行計算 / Debugging schemes / Multi-threading / Message passing / MIMD machine / Parallel language / f language / Compiler implementation / AP1000 / スーパーコンピューティング / 実行支援系 / MIMD / コンパイラ / 超並列計算機 / 並列オブジェクト言語 / ガ-ベジコレクション / ユンパイラ / 起並列MIMD型計算機 / Schematic / デバッグ方式 / f / ASCL / 言語処理系 / 超並列MIMD型計算機 / デバギング方式 / マルチ・スレディング / メッセージ送受信 / MIMD計算機 / f言語 / コンパイラ実装隠す

検証指向プログラミング言語の設計と実装研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  2026 – 2030
- 研究種目
  
  基盤研究(A)
- 審査区分
  
  中区分60:情報科学、情報工学およびその関連分野
- 研究機関
  東京大学
高階不動点論理に基づくプログラム検証研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  2020
- 研究種目
  
  基盤研究(A)
- 審査区分
  
  中区分60:情報科学、情報工学およびその関連分野
- 研究機関
  東京大学
AI時代を見据えたプログラム検証技術研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  2020 – 2024
- 研究種目
  
  基盤研究(S)
- 審査区分
  
  大区分J
- 研究機関
  東京大学
高階モデル検査の深化と発展研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  2015 – 2019
- 研究種目
  
  基盤研究(S)
- 研究分野
  
  情報学基礎理論
- 研究機関
  東京大学
クラス理論に基づく自己拡張可能なソフトウェア検証体系の構築
- 研究代表者
  
  佐藤雅彦
- 研究期間 (年度)
  2013 – 2016
- 研究種目
  
  基盤研究(B)
- 研究分野
  
  ソフトウェア
- 研究機関
  京都大学
高階モデル検査とその応用研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  2011 – 2015
- 研究種目
  
  基盤研究(S)
- 研究分野
  
  情報学基礎
- 研究機関
  東京大学
   東北大学
ソフトウェアの安全性向上のための型理論の深化と応用研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  2008 – 2010
- 研究種目
  
  基盤研究(A)
- 研究分野
  
  情報学基礎
- 研究機関
  東北大学
順序付き線形型に基づく安全かつ高速な大規模データ処理の実現研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  2007 – 2008
- 研究種目
  
  特定領域研究
- 審査区分
  
  理工系
- 研究機関
  東北大学
順序付き線形型に基づく安全かつ高速な大規模データ処理の実現研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  2006
- 研究種目
  
  特定領域研究
- 審査区分
  
  理工系
- 研究機関
  東北大学
ソフトウェアの安全性向上のための型理論研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  2005 – 2007
- 研究種目
  
  基盤研究(B)
- 研究分野
  
  ソフトウエア
- 研究機関
  東北大学
型システムとモデル検査の融合によるソフトウェア検証研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  2004 – 2006
- 研究種目
  
  萌芽研究
- 研究分野
  
  ソフトウエア
- 研究機関
  東北大学
日米科学協力事業「ソフトウェア検証の論理的方法」更新のための企画研究
- 研究代表者
  
  岡田光弘
- 研究期間 (年度)
  2003
- 研究種目
  
  基盤研究(C)
- 研究分野
  
  情報学基礎
- 研究機関
  慶應義塾大学
充実期を迎えた線形論理の進化とその応用に関する研究
- 研究代表者
  
  岡田光弘
- 研究期間 (年度)
  2003 – 2005
- 研究種目
  
  基盤研究(B)
- 研究分野
  
  ソフトウエア
- 研究機関
  慶應義塾大学
プログラム解析のための統一型理論の構築・検証とそれに基づく解析器の自動合成研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  2002 – 2004
- 研究種目
  
  若手研究(A)
- 研究分野
  
  計算機科学
- 研究機関
  東北大学
   東京工業大学
セキュアコンピューティングのための型システム研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  2000 – 2003
- 研究種目
  
  特定領域研究
- 審査区分
  
  理工系
- 研究機関
  東京工業大学
高性能広域分散計算のための適応的な基盤ソフトウェア
- 研究代表者
  
  米澤明憲
- 研究期間 (年度)
  2000 – 2002
- 研究種目
  
  基盤研究(A)
- 研究分野
  
  計算機科学
- 研究機関
  東京大学
線形論理を用いた並行計算システム及び実時間システムの形式仕様・形式検証の理論
- 研究代表者
  
  岡田光弘
- 研究期間 (年度)
  2000 – 2002
- 研究種目
  
  基盤研究(B)
- 研究分野
  
  計算機科学
- 研究機関
  慶應義塾大学
疑似線形型システムに基づくメモリ管理とプログラム最適化研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  1999 – 2001
- 研究種目
  
  基盤研究(B)
- 研究分野
  
  計算機科学
- 研究機関
  東京工業大学
   東京大学
様相線形論理に基づく分散計算モデルおよび型システムの研究研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  1998
- 研究種目
  
  特定領域研究(A)
- 研究機関
  東京大学
並行・分散計算の先進的理論に基づく分散プログラミング言語処理系の構築研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  1998 – 2000
- 研究種目
  
  基盤研究(B)
- 研究分野
  
  計算機科学
- 研究機関
  東京工業大学
   東京大学
様相線形論理に基づく分散計算モデルおよび型システムの研究研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  1997
- 研究種目
  
  重点領域研究
- 研究機関
  東京大学
先進的型システムに基づく並列プログラミング言語のデバッガ及びメモリ管理の研究研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  1997 – 1998
- 研究種目
  
  奨励研究(A)
- 研究分野
  
  計算機科学
- 研究機関
  東京大学
非同期通信に基づく並列言語の静的解析とそれに基づく最適化研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  1996
- 研究種目
  
  奨励研究(A)
- 研究分野
  
  計算機科学
- 研究機関
  東京大学
同期チャネルとオブジェクトを持つ並列言語の分散共有記憶型並列計算機上の高効率実現
- 研究代表者
  
  米澤明憲
- 研究期間 (年度)
  1996 – 1998
- 研究種目
  
  基盤研究(A)
- 研究分野
  
  計算機科学
- 研究機関
  東京大学
線形論理プログラミングHACLに基づく型つき並列オブジェクト指向言語の実装研究代表者
- 研究代表者
  
  小林直樹
- 研究期間 (年度)
  1995
- 研究種目
  
  奨励研究(A)
- 研究分野
  
  計算機科学
- 研究機関
  東京大学
線形論理に基づく並列計算の枠組み及びプログラミング言語の設計・実装に関する研究
- 研究代表者
  
  米澤明憲
- 研究期間 (年度)
  1994 – 1995
- 研究種目
  
  一般研究(B)
- 研究分野
  
  計算機科学
- 研究機関
  東京大学
並列オブジェクト指向言語処理系の汎用MIMP型並列計算機上での高効率な実現
- 研究代表者
  
  米澤明憲
- 研究期間 (年度)
  1993 – 1995
- 研究種目
  
  試験研究(B)
- 研究分野
  
  計算機科学
- 研究機関
  東京大学

[雑誌論文] Ownership Types for Verification of Programs with Pointer Arithmetic2024
- 著者名/発表者名
  Tanaka Izumi、Sakayori Ken、Kobayashi Naoki
- 雑誌名
  
  Proceedings of PEPM 2024, ACM
  
  巻: - ページ: 94-106
- DOI
  10.1145/3635800.3636965
- 査読あり
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] Borrowable Fractional Ownership Types for Verification2024
- 著者名/発表者名
  Takashi Nakayama, Yusuke Matsushita, Ken Sakayori, Ryosuke Sato and Naoki Kobayashi
- 雑誌名
  
  VMCAI 2024, Lecture Notes in Computer Science
  
  巻: 14500 ページ: 224-246
- DOI
  10.1007/978-3-031-50521-8_11
- ISBN
  9783031505201, 9783031505218
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-22KJ0561, KAKENHI-PROJECT-20H05703
[雑誌論文] 命令型プログラムの安全性検証のための所有権主導変換2024
- 著者名/発表者名
  小林亮太, 中村烈士, 五十嵐淳, 末永幸平, 小林直樹
- 雑誌名
  
  第26回プログラミングおよびプログラミング言語ワークショップ(PPL2024)論文集
  
  巻: -
- 査読あり
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] Asynchronous unfold/fold transformation for fixpoint logic2024
- 著者名/発表者名
  Faisal Al Ameen Mahmudul、Kobayashi Naoki、Sato Ryosuke
- 雑誌名
  
  Science of Computer Programming
  
  巻: 231 ページ: 103014-103014
- DOI
  10.1016/j.scico.2023.103014
- 査読あり
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] Productivity Verification for Functional Programs by Reduction to Termination Verification2024
- 著者名/発表者名
  Fukaishi Ren、Kobayashi Naoki、Sato Ryosuke
- 雑誌名
  
  Proceedings of PEPM 2024, ACM
  
  巻: - ページ: 70-82
- DOI
  10.1145/3635800.3636963
- 査読あり
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] Argument Reduction of Constrained Horn Clauses Using Equality Constraints2023
- 著者名/発表者名
  Ikeda Ryo、Sato Ryosuke、Kobayashi Naoki
- 雑誌名
  
  Proceedings of APLAS 2023, Springer LNCS
  
  巻: 14405 ページ: 246-265
- DOI
  10.1007/978-981-99-8311-7_12
- ISBN
  9789819983100, 9789819983117
- 査読あり
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] Neural Network-Guided Synthesis of Recursive List Functions2023
- 著者名/発表者名
  Naoki Kobayashi, Minchao Wu
- 雑誌名
  
  Proceedings of TACAS 2023, Springer LNCS
  
  巻: 13993 ページ: 227-245
- DOI
  10.1007/978-3-031-30823-9_12
- ISBN
  9783031308222, 9783031308239
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] Higher-Order Property-Directed Reachability2023
- 著者名/発表者名
  Katsura Hiroyuki、Kobayashi Naoki、Sato Ryosuke
- 雑誌名
  
  Proceedings of the ACM on Programming Languages
  
  巻: 7 号: ICFP ページ: 48-77
- DOI
  10.1145/3607831
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-23KJ0546, KAKENHI-PROJECT-20H05703
[雑誌論文] HFL(Z) Validity Checking for Automated Program Verification2023
- 著者名/発表者名
  Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, and Takeshi Tsukada
- 雑誌名
  
  Proceedings of the ACM on Programming Languages, Issue POPL, ACM
  
  巻: 7 号: POPL ページ: 154-184
- DOI
  10.1145/3571199
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] Gradual Tensor Shape Checking2023
- 著者名/発表者名
  Momoko Hattori, Naoki Kobayashi, Ryosuke Sato
- 雑誌名
  
  Proceedings of ESOP 2023, Springer LNCS
  
  巻: 13990 ページ: 197-224
- DOI
  10.1007/978-3-031-30044-8_8
- ISBN
  9783031300431, 9783031300448
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] On Higher-Order Reachability Games Vs May Reachability2022
- 著者名/発表者名
  Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi
- 雑誌名
  
  Proceedings of RP 2022, Springer LNCS
  
  巻: 13608 ページ: 108-124
- DOI
  10.1007/978-3-031-19135-0_8
- ISBN
  9783031191343, 9783031191350
- 査読あり
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] Parameterized Recursive Refinement Types for Automated Program Verification2022
- 著者名/発表者名
  Ryoya Mukai, Naoki Kobayashi, Ryosuke Sato
- 雑誌名
  
  Proceedings of SAS 2022, Springer LNCS
  
  巻: 13790 ページ: 397-421
- DOI
  10.1007/978-3-031-22308-2_18
- ISBN
  9783031223075, 9783031223082
- 査読あり
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] Asynchronous Unfold/Fold Transformation for Fixpoint Logic2022
- 著者名/発表者名
  Mahmudul Faisal Al Ameen, Naoki Kobayashi, Ryosuke Sato
- 雑誌名
  
  Proceedings of FLOPS 2022, Springer LNCS
  
  巻: 13215 ページ: 39-56
- DOI
  10.1007/978-3-030-99461-7_3
- ISBN
  9783030994600, 9783030994617
- 査読あり
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] Symbolic Automatic Relations and Their Applications to SMT and CHC Solving2021
- 著者名/発表者名
  Shimoda Takumi、Kobayashi Naoki、Sakayori Ken、Sato Ryosuke
- 雑誌名
  
  Proceedings of SAS 2021, Springer LNCS
  
  巻: 12913 ページ: 405-428
- DOI
  10.1007/978-3-030-88806-0_20
- ISBN
  9783030888053, 9783030888060
- 査読あり
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] Toward Neural-Network-Guided Program Synthesis and Verification2021
- 著者名/発表者名
  Kobayashi Naoki、Sekiyama Taro、Sato Issei、Unno Hiroshi
- 雑誌名
  
  Lecture Notes in Computer Science (SAS)
  
  巻: 12913 ページ: 236-260
- DOI
  10.1007/978-3-030-88806-0_12
- ISBN
  9783030888053, 9783030888060
- 査読あり
- データソース
  KAKENHI-PROJECT-19K20247, KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-23K20380
[雑誌論文] Counterexample generation for program verification based on ownership refinement types2021
- 著者名/発表者名
  Ueno Hideto、Toman John、Kobayashi Naoki、Tsukada Takeshi
- 雑誌名
  
  Proceedings of PEPM 2021, ACM Press
  
  巻: - ページ: 44-57
- DOI
  10.1145/3441296.3441396
- 査読あり
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] Inside-Outside Algorithm for Macro Grammars2021
- 著者名/発表者名
  Ryuta Kambe, Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, Ryo Yoshinaka
- 雑誌名
  
  Proceedings of Machine Learning Research
  
  巻: 153 ページ: 32-46
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes2021
- 著者名/発表者名
  Patrick Baillot, Alexis Ghyselen, Naoki Kobayashi
- 雑誌名
  
  Proceedings of CONCUR 2021, LIPIcs
  
  巻: 203
- 査読あり / オープンアクセス / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] A Probabilistic Higher-order Fixpoint Logic2021
- 著者名/発表者名
  Mitani Yo、Kobayashi Naoki、Tsukada Takeshi
- 雑誌名
  
  Logical Methods in Computer Science
  
  巻: Volume 17, Issue 4 ページ: 1-36
- DOI
  10.46298/lmcs-17(4:15)2021
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] A Cyclic Proof System for HFL_N2021
- 著者名/発表者名
  Mayuko Kori, Takeshi Tsukada, and Naoki Kobayashi
- 雑誌名
  
  Proceedings of CONCUR 2021, LIPIcs
  
  巻: 203
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination2021
- 著者名/発表者名
  Shoshi Tsubasa、Ishikawa Takuma、Kobayashi Naoki、Sakayori Ken、Sato Ryosuke、Tsukada Takeshi
- 雑誌名
  
  Proceedings of APLAS 2021, Springer LNCS
  
  巻: 13008 ページ: 265-284
- DOI
  10.1007/978-3-030-89051-3_15
- ISBN
  9783030890506, 9783030890513
- 査読あり
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] RustHorn: CHC-based Verification for Rust Programs2021
- 著者名/発表者名
  Matsushita Yusuke、Tsukada Takeshi、Kobayashi Naoki
- 雑誌名
  
  ACM Transactions on Programming Languages and Systems
  
  巻: 43 号: 4 ページ: 1-54
- DOI
  10.1145/3462205
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-22KJ0561
[雑誌論文] An Overview of the HFL Model Checking Project2021
- 著者名/発表者名
  Kobayashi Naoki
- 雑誌名
  
  Electronic Proceedings in Theoretical Computer Science
  
  巻: 344 ページ: 1-12
- DOI
  10.4204/eptcs.344.1
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-20H05703
[雑誌論文] A New Refinement Type System for Automated nu-HFLZ Validity Checking2020
- 著者名/発表者名
  Hiroyuki Katsura, Naoki Iwayama, Naoki Kobayashi, and Takeshi Tsukada
- 雑誌名
  
  Proceedings of APLAS 2020, Springer LNCS
  
  巻: 12470
- 査読あり
- データソース
  KAKENHI-PROJECT-20H00577
[雑誌論文] ICE-Based Refinement Type Discovery for Higher-Order Functional Programs2020
- 著者名/発表者名
  Champion Adrien、Chiba Tomoya、Kobayashi Naoki、Sato Ryosuke
- 雑誌名
  
  Journal of Automated Reasoning
  
  巻: 64 号: 7 ページ: 1393-1418
- DOI
  10.1007/s10817-020-09571-y
- 査読あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs2020
- 著者名/発表者名
  Toman John、Siqi Ren、Suenaga Kohei、Igarashi Atsushi、Kobayashi Naoki
- 雑誌名
  
  Proceedings of ESOP 2020, Springer LNCS
  
  巻: 12075 ページ: 684-714
- DOI
  10.1007/978-3-030-44914-8_25
- NAID
  120006879514
- ISBN
  9783030449131, 9783030449148
- 査読あり / オープンアクセス / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15H05706, KAKENHI-PROJECT-19H04084
[雑誌論文] Fold/Unfold Transformations for Fixpoint Logic2020
- 著者名/発表者名
  Kobayashi Naoki、Fedyukovich Grigory、Gupta Aarti
- 雑誌名
  
  Proceedings of TACAS 2020, Springer LNCS
  
  巻: 12079 ページ: 195-214
- DOI
  10.1007/978-3-030-45237-7_12
- ISBN
  9783030452360, 9783030452377
- 査読あり / オープンアクセス / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] On Average-Case Hardness of Higher-Order Model Checking2020
- 著者名/発表者名
  Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada
- 雑誌名
  
  Proceedings of FSCD 2020, LIPIcs
  
  巻: 167
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Predicate Abstraction and CEGAR for nuHFL(Z) Validity Checking2020
- 著者名/発表者名
  Naoki Iwayama, Naoki Kobayashi, Ryota Suzuki and Takeshi Tsukada
- 雑誌名
  
  Proceedings of SAS 2020, Springer LNCS
  
  巻: 12389
- 査読あり
- データソース
  KAKENHI-PROJECT-20H00577
[雑誌論文] Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars2020
- 著者名/発表者名
  Kazuyuki Asada and Naoki Kobayashi
- 雑誌名
  
  Proceedings of FSCD 2020, LIPIcs
  
  巻: 167
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] RustHorn: CHC-Based Verification for Rust Programs2020
- 著者名/発表者名
  Matsushita Yusuke、Tsukada Takeshi、Kobayashi Naoki
- 雑誌名
  
  Proceedings of ESOP 2020, Springer LNCS
  
  巻: 12075 ページ: 484-514
- DOI
  10.1007/978-3-030-44914-8_18
- ISBN
  9783030449131, 9783030449148
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Grammar Compression with Probabilistic Context-Free Grammar2020
- 著者名/発表者名
  Naganuma Hiroaki、Hendrian Diptarama、Yoshinaka Ryo、Shinohara Ayumi、Kobayashi Naoki
- 雑誌名
  
  Proceedings of DCC 2020, IEEE
  
  巻: - ページ: 386-386
- DOI
  10.1109/dcc47342.2020.00093
- 査読あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] A Probabilistic Higher-Order Fixpoint Logic2020
- 著者名/発表者名
  Yo Mitani, Naoki Kobayashi, and Takeshi Tsukada
- 雑誌名
  
  Proceedings of FSCD 2020, LIPIcs
  
  巻: 167
- 査読あり
- データソース
  KAKENHI-PROJECT-20H00577
[雑誌論文] A Probabilistic Higher-Order Fixpoint Logic2020
- 著者名/発表者名
  Yo Mitani, Naoki Kobayashi, Takeshi Tsukada
- 雑誌名
  
  Proceedings of FSCD 2020, LIPIcs
  
  巻: 167
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence2019
- 著者名/発表者名
  Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada
- 雑誌名
  
  Logical Methods in Computer Science
  
  巻: 15
- DOI
  10.23638/lmcs-15(1:16)2019
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] An improvement of the Franek-Jennings-Smyth pattern matching algorithm2019
- 著者名/発表者名
  Satoshi Kobayashi, Diptarama Hendrian, Ryo Yoshinaka, and Ayumi Shinohara
- 雑誌名
  
  Proceedings of the Prague Stringology Conference 2019 (PSC 2019)
  
  巻: - ページ: 56-68
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Reduction from branching-time property verification of higher-order programs to HFL validity checking2019
- 著者名/発表者名
  Watanabe Keiichi、Tsukada Takeshi、Oshikawa Hiroki、Kobayashi Naoki
- 雑誌名
  
  Proceedings of PEPM 2019
  
  巻: - ページ: 22-34
- DOI
  10.1145/3294032.3294077
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] A Type-Based HFL Model Checking Algorithm2019
- 著者名/発表者名
  Hosoi Youkichi、Kobayashi Naoki、Tsukada Takeshi
- 雑誌名
  
  Proceedings of APLAS 2019, Springer LNCS
  
  巻: 11893 ページ: 136-155
- DOI
  10.1007/978-3-030-34175-6_8
- ISBN
  9783030341749, 9783030341756
- 査読あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] A Temporal Logic for Higher-Order Functional Programs2019
- 著者名/発表者名
  Okuyama Yuya、Tsukada Takeshi、Kobayashi Naoki
- 雑誌名
  
  Proceedings of SAS 2019, Springer LNCS
  
  巻: 11822 ページ: 437-458
- DOI
  10.1007/978-3-030-32304-2_21
- ISBN
  9783030323035, 9783030323042
- 査読あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] On the Termination Problem for Probabilistic Higher-Order Recursive Programs2019
- 著者名/発表者名
  Kobayashi Naoki、Dal Lago Ugo、Grellois Charles
- 雑誌名
  
  Proceedings of LICS 2019
  
  巻: - ページ: 1-14
- DOI
  10.1109/lics.2019.8785679
- 査読あり / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Temporal Verification of Programs via First-Order Fixpoint Logic2019
- 著者名/発表者名
  Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, Hiroshi Unno
- 雑誌名
  
  In Proceedings of the 26th International Symposium (SAS 2019), Lecture Notes in Computer Science
  
  巻: 11822 ページ: 413-436
- DOI
  10.1007/978-3-030-32304-2_20
- ISBN
  9783030323035, 9783030323042
- 査読あり
- データソース
  KAKENHI-PROJECT-17H01720, KAKENHI-PROJECT-16H05856, KAKENHI-PROJECT-15H05706
[雑誌論文] Combining higher-order model checking with refinement type inference2019
- 著者名/発表者名
  Sato Ryosuke、Iwayama Naoki、Kobayashi Naoki
- 雑誌名
  
  Proceedings of PEPM 2019
  
  巻: - ページ: 47-53
- DOI
  10.1145/3294032.3294081
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Higher-Order Program Verification via HFL Model Checking2018
- 著者名/発表者名
  Kobayashi Naoki、Tsukada Takeshi、Watanabe Keiichi
- 雑誌名
  
  Proceedings of the 27th European Symposium on Programming
  
  巻: 0 ページ: 711-738
- DOI
  10.1007/978-3-319-89884-1_25
- ISBN
  9783319898834, 9783319898841
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-16K16004, KAKENHI-PROJECT-15H05706
[雑誌論文] HoIce: An ICE-Based Non-linear Horn Clause Solver2018
- 著者名/発表者名
  Champion Adrien、Kobayashi Naoki、Sato Ryosuke
- 雑誌名
  
  Proceedings of APLAS 2018, Springer LNCS
  
  巻: 11275 ページ: 146-156
- DOI
  10.1007/978-3-030-02768-1_8
- ISBN
  9783030027674, 9783030027681
- 査読あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Automated Synthesis of Functional Programs with Auxiliary Functions2018
- 著者名/発表者名
  Eguchi Shingo、Kobayashi Naoki、Tsukada Takeshi
- 雑誌名
  
  Proceedings of APLAS 2018, Springer LNCS
  
  巻: 11275 ページ: 223-241
- DOI
  10.1007/978-3-030-02768-1_13
- ISBN
  9783030027674, 9783030027681
- 査読あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] ICE-Based Refinement Type Discovery for Higher-Order Functional Programs2018
- 著者名/発表者名
  Champion Adrien、Chiba Tomoya、Kobayashi Naoki、Sato Ryosuke
- 雑誌名
  
  Proceedings of TACAS 2018, Springer LNCS
  
  巻: 10805 ページ: 365-384
- DOI
  10.1007/978-3-319-89960-2_20
- ISBN
  9783319899596, 9783319899602
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered2018
- 著者名/発表者名
  Kazuyuki Asada, Naoki Kobayashi
- 雑誌名
  
  Proceedings of the 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
  
  巻: LIPIcs 122 ページ: 1-15
- DOI
  10.4230/LIPICS.FSTTCS.2018.14
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-18K11156, KAKENHI-PROJECT-15H05706
[雑誌論文] Deadlock analysis of unbounded process networks2017
- 著者名/発表者名
  Kobayashi Naoki、Laneve Cosimo
- 雑誌名
  
  Information and Computation
  
  巻: 252 ページ: 48-70
- DOI
  10.1016/j.ic.2016.03.004
- 査読あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence2017
- 著者名/発表者名
  Sin’ya Ryoma, Asada Kazuyuki, Kobayashi Naoki and Tsukada Takeshi
- 雑誌名
  
  Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures
  
  巻: 0 ページ: 53-68
- DOI
  10.1007/978-3-662-54458-7_4
- ISBN
  9783662544570, 9783662544587
- 査読あり
- データソース
  KAKENHI-PROJECT-16K16004, KAKENHI-PROJECT-15H05706
[雑誌論文] Modular Verification of Higher-Order Functional Programs2017
- 著者名/発表者名
  Sato Ryosuke、Kobayashi Naoki
- 雑誌名
  
  Proceedings of ESOP 2017, Springer LNCS
  
  巻: 10201 ページ: 831-854
- DOI
  10.1007/978-3-662-54434-1_31
- ISBN
  9783662544334, 9783662544341
- 査読あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Streett Automata Model Checking of Higher-Order Recursion Schemes2017
- 著者名/発表者名
  Ryota Suzuki, Koichi Fujima, Naoki Kobayashi and Takeshi Tsukada
- 雑誌名
  
  Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction
  
  巻: 0
- DOI
  10.4230/LIPIcs.FSCD.2017.32
- 査読あり
- データソース
  KAKENHI-PROJECT-16K16004, KAKENHI-PROJECT-15H05706
[雑誌論文] On the relationship between higher-order recursion schemes and higher-order fixpoint logic2017
- 著者名/発表者名
  Kobayashi Naoki、Lozes Etienne、Bruse Florian
- 雑誌名
  
  Proceedings of POPL 2017
  
  巻: - ページ: 246-259
- DOI
  10.1145/3009837.3009854
- 査読あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Verifying relational properties of functional programs by first-order refinement2017
- 著者名/発表者名
  Asada Kazuyuki、Sato Ryosuke、Kobayashi Naoki
- 雑誌名
  
  Science of Computer Programming
  
  巻: 137 ページ: 2-62
- DOI
  10.1016/j.scico.2016.02.007
- 査読あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Pumping Lemma for Higher-Order Languages2017
- 著者名/発表者名
  Kazuyuki Asada and Naoki Kobayashi
- 雑誌名
  
  Proceedings of ICALP 2017, LIPIcs
  
  巻: 80
- DOI
  10.4230/LIPIcs.ICALP.2017.97
- 査読あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Verification of code generators via higher-order model checking2017
- 著者名/発表者名
  Suwa Takashi、Tsukada Takeshi、Kobayashi Naoki、Igarashi Atsushi
- 雑誌名
  
  Proceedings of PEPM 2017
  
  巻: - ページ: 59-70
- DOI
  10.1145/3018882.3018886
- 査読あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation2016
- 著者名/発表者名
  Kazuhide Yasukata, Takeshi Tsukada and Naoki Kobayashi
- 雑誌名
  
  Programming Languages and Systems
  
  巻: 10017 of LNCS ページ: 335-353
- DOI
  10.1007/978-3-319-47958-3_18
- ISBN
  9783319479576, 9783319479583
- 査読あり / 謝辞記載あり
- データソース
  KAKENHI-PROJECT-16K16004, KAKENHI-PROJECT-15H05706
[雑誌論文] Higher-Order Model Checking in Direct Style2016
- 著者名/発表者名
  Taku Terao, Taskeshi Tsukada, and Naoki Kobayashi
- 雑誌名
  
  Proceedings of APLAS 2014, LNCS
  
  巻: 10017 ページ: 295-313
- DOI
  10.1007/978-3-319-47958-3_16
- ISBN
  9783319479576, 9783319479583
- 査読あり / 謝辞記載あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-16J01038, KAKENHI-PROJECT-15H05706
[雑誌論文] Automatically disproving fair termination of higher-order functional programs2016
- 著者名/発表者名
  Watanabe Keiichi、Sato Ryosuke、Tsukada Takeshi、Kobayashi Naoki
- 雑誌名
  
  Proceedings of ICFP 2016
  
  巻: - ページ: 243-255
- DOI
  10.1145/2951913.2951919
- 査読あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Compact bit encoding schemes for simply-typed lambda-terms2016
- 著者名/発表者名
  Takeda Kotaro、Kobayashi Naoki、Yaguchi Kazuya、Shinohara Ayumi
- 雑誌名
  
  Proceedings of ICFP 2016
  
  巻: - ページ: 146-157
- DOI
  10.1145/2951913.2951918
- 査読あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Temporal Verification of Higher-Order Functional Programs2016
- 著者名/発表者名
  Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno
- 雑誌名
  
  In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), ACM SIGPLAN Notices
  
  巻: 51 (1) ページ: 57-68
- DOI
  10.1145/2837614.2837667
- 査読あり / 謝辞記載あり / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-26330082, KAKENHI-PROJECT-15H05706, KAKENHI-PROJECT-25730035, KAKENHI-PROJECT-25280020, KAKENHI-PROJECT-25280023
[雑誌論文] Equivalence-Based Abstraction Refinement for muHORS Model Checking2016
- 著者名/発表者名
  Li Xin、Kobayashi Naoki
- 雑誌名
  
  Proceedings of ATVA 2016, Springer LNCS
  
  巻: 9938 ページ: 304-320
- DOI
  10.1007/978-3-319-46520-3_20
- ISBN
  9783319465197, 9783319465203
- 査読あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] On Word and Frontier Languages of Unsafe Higher-Order Grammars2016
- 著者名/発表者名
  Kazuyuki Asada、Naoki Kobayashi
- 雑誌名
  
  Proceedings of ICALP 2016
  
  巻: -
- DOI
  10.4230/LIPIcs.ICALP.2016.111
- 査読あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Refinement Type Checking via Assertion Checking2015
- 著者名/発表者名
  Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi
- 雑誌名
  
  Journal of Information Processing
  
  巻: 23 号: 6 ページ: 827-834
- DOI
  10.2197/ipsjjip.23.827
- NAID
  130005109162
- ISSN
  1882-6652
- 言語
  英語
- 査読あり / 謝辞記載あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Decision Algorithms for Checking Definability of Order-2 Finitary PCF2015
- 著者名/発表者名
  Sadaaki Kawata, Kazuyuki Asada, Naoki Kobayashi
- 雑誌名
  
  Proceedings of APLAS 2015, LNCS
  
  巻: 9458 ページ: 313-331
- DOI
  10.1007/978-3-319-26529-2_17
- ISBN
  9783319265285, 9783319265292
- 査読あり / 謝辞記載あり
- データソース
  KAKENHI-PROJECT-15H05706
[雑誌論文] Verification of Tree-Processing Programs via Higher-Order Mode Checking2015
- 著者名/発表者名
  Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
- 雑誌名
  
  Mathematical Structures in Computer Science
  
  巻: Volume 25, Special Issue 04 号: 4 ページ: 841-866
- DOI
  10.1017/s0960129513000054
- 査読あり
- データソース
  KAKENHI-PROJECT-25730035, KAKENHI-PROJECT-23220001
[雑誌論文] Automata-based Abstraction Refinement for muHORS Model Checking2015
- 著者名/発表者名
  Naoki Kobayashi, Xin Li
- 雑誌名
  
  Proceedings of LICS 2015
  
  巻: 未定
- 査読あり / 謝辞記載あり
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] 高階木変換器の自動検証のための反例発見と抽象化改良2015
- 著者名/発表者名
  松本雄磨, 小林直樹, 海野広志
- 雑誌名
  
  コンピュータソフトウェア
  
  巻: 32 号: 1 ページ: 1_161-1_178
- DOI
  10.11309/jssst.32.1_161
- NAID
  130004892316
- ISSN
  0289-6540
- 言語
  日本語
- 査読あり / 謝辞記載あり
- データソース
  KAKENHI-PROJECT-25730035, KAKENHI-PROJECT-23220001
[雑誌論文] Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs2015
- 著者名/発表者名
  Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
- 雑誌名
  
  Proceedings of CAV 2015, LNCS
  
  巻: 9207 ページ: 287-303
- DOI
  10.1007/978-3-319-21668-3_17
- ISBN
  9783319216676, 9783319216683
- 査読あり / 謝辞記載あり
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs2015
- 著者名/発表者名
  Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno
- 雑誌名
  
  Proceedings of APLAS 2015, LNCS
  
  巻: 9458 ページ: 295-312
- DOI
  10.1007/978-3-319-26529-2_16
- ISBN
  9783319265285, 9783319265292
- 査読あり / 謝辞記載あり
- データソース
  KAKENHI-PROJECT-15H05706, KAKENHI-PROJECT-25730035
[雑誌論文] Verifying Relational Properties of Functional Programs by First-Order Refinement2015
- 著者名/発表者名
  Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi
- 雑誌名
  
  Proceedings of PEPM 2015
  
  巻: なしページ: 61-72
- DOI
  10.1145/2678015.2682546
- 査読あり / 謝辞記載あり
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] Complexity of Model-Checking Call-by-Value Programs2014
- 著者名/発表者名
  Takeshi Tsukada, Naoki Kobayashi
- 雑誌名
  
  Proceedings of FoSSaCS 2014, LNCS
  
  巻: 8412 ページ: 180-194
- DOI
  10.1007/978-3-642-54830-7_12
- ISBN
  9783642548291, 9783642548307
- 査読あり / 謝辞記載あり
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] Pairwise Reachability Analysis for Higher Order Concurrent Programs by Higher-Order Model Checking2014
- 著者名/発表者名
  Kazuhide Yasukata, Naoki Kobayashi, Kazutaka Matsuda
- 雑誌名
  
  Proceedings of CONCUR 2014, LNCS
  
  巻: 8704 ページ: 312-326
- DOI
  10.1007/978-3-662-44584-6_22
- ISBN
  9783662445839, 9783662445846
- 査読あり / 謝辞記載あり
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] Efficient Algorithm and Coding for Higher-Order Compression2014
- 著者名/発表者名
  Kazuya Yaguchi, Naoki Kobayashi, Ayumi Shinohara
- 雑誌名
  
  Proceedings of DCC 2014
  
  巻: なしページ: 434-434
- DOI
  10.1109/dcc.2014.63
- NAID
  110009820601
- 査読あり
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] Unsafe Order-2 Tree Languages Are Context-Sensitive2014
- 著者名/発表者名
  Naoki Kobayashi, Kazuhiro Inaba, Takeshi Tsukada
- 雑誌名
  
  Proceedings of FoSSaCS 2014, LNCS
  
  巻: 8412 ページ: 149-163
- DOI
  10.1007/978-3-642-54830-7_10
- ISBN
  9783642548291, 9783642548307
- 査読あり / 謝辞記載あり
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] A ZDD-Based Efficient Higher-Order Model Checking Algorithm2014
- 著者名/発表者名
  Taku Terao, Naoki Kobayashi
- 雑誌名
  
  Proceedings of APLAS 2014, LNCS
  
  巻: 8858 ページ: 354-371
- DOI
  10.1007/978-3-319-12736-1_19
- ISBN
  9783319127354, 9783319127361
- 査読あり / 謝辞記載あり
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] Deadlock Analysis of Unbounded Process Networks2014
- 著者名/発表者名
  Elena Giachino, Naoki Kobayashi, Cosimo Laneve
- 雑誌名
  
  Proceedings of CONCUR 2014, LNCS
  
  巻: 8704 ページ: 63-77
- DOI
  10.1007/978-3-662-44584-6_6
- ISBN
  9783662445839, 9783662445846
- 査読あり / 謝辞記載あり / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] Automatic Termination Verification for Higher-Order Functional Programs2014
- 著者名/発表者名
  Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi
- 雑誌名
  
  Proceedings of ESOP 2014, LNCS
  
  巻: 8410 ページ: 392-411
- DOI
  10.1007/978-3-642-54833-8_21
- ISBN
  9783642548321, 9783642548338
- 査読あり / 謝辞記載あり
- データソース
  KAKENHI-PROJECT-23220001, KAKENHI-PROJECT-23700026, KAKENHI-PROJECT-25280023, KAKENHI-PROJECT-25730035, KAKENHI-PROJECT-26330082
[雑誌論文] Model-Checking Higher-Order Programs with Recursive Types2013
- 著者名/発表者名
  Naoki Kobayashi, Atsushi Igarashi
- 雑誌名
  
  Proceedings of ESOP 2013, LNCS
  
  巻: 7792 ページ: 431-450
- DOI
  10.1007/978-3-642-37036-6_24
- ISBN
  9783642370359, 9783642370366
- 査読あり
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] Saturation-Based Model Checking of Higher-Order Recursion Schemes2013
- 著者名/発表者名
  Christopher H. Broadbent, Naoki Kobayashi
- 雑誌名
  
  Proceedings of CSL 2013, LIPIcs
  
  巻: 23 ページ: 129-148
- DOI
  10.4230/LIPIcs.CSL.2013.129
- 査読あり
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes2013
- 著者名/発表者名
  Koichi Fujima, Sohei Ito, Naoki Kobayashi
- 雑誌名
  
  Proceedings of APLAS 2013, LNCS
  
  巻: 8301 ページ: 17-32
- DOI
  10.1007/978-3-319-03542-0_2
- ISBN
  9783319035413, 9783319035420
- 査読あり
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] Model Checking Higher-Order Programs2013
- 著者名/発表者名
  Naoki Kobayashi
- 雑誌名
  
  Journal of the ACM
  
  巻: 60(3) 号: 3 ページ: 1-62
- DOI
  10.1145/2487241.2487246
- 査読あり
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] Automating relatively complete verification of higher-order functional programs2013
- 著者名/発表者名
  Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
- 雑誌名
  
  Proceedings of The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13
  
  巻: - ページ: 75-86
- DOI
  10.1145/2429069.2429081
- NAID
  120007136948
- 査読あり
- データソース
  KAKENHI-PROJECT-23220001, KAKENHI-PROJECT-23700026
[雑誌論文] Pumping by Typing2013
- 著者名/発表者名
  Naoki Kobayashi
- 雑誌名
  
  2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science
  
  巻: - ページ: 398-407
- DOI
  10.1109/lics.2013.46
- 査読あり
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] Towards a scalable software model checker for higher-order programs2013
- 著者名/発表者名
  Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
- 雑誌名
  
  Proceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation (PEPM 2013)
  
  巻: - ページ: 56-62
- DOI
  10.1145/2426890.2426900
- 査読あり
- データソース
  KAKENHI-PROJECT-12J08057, KAKENHI-PROJECT-23220001
[雑誌論文] An Intersection Type System for Deterministic Pushdown Automata2012
- 著者名/発表者名
  Takeshi Tsukada
- 雑誌名
  
  Proceedings of IFIP-TCS 2012, LNCS
  
  巻: 7604 ページ: 357-371
- DOI
  10.1007/978-3-642-33475-7_25
- ISBN
  9783642334740, 9783642334757
- 査読あり
- データソース
  KAKENHI-PROJECT-10J03842, KAKENHI-PROJECT-23220001
[雑誌論文] Functional programs as compressed data2012
- 著者名/発表者名
  Naoki Kobayashi
- 雑誌名
  
  PEPM 2012
  
  巻: - ページ: 121-130
- DOI
  10.1145/2103746.2103770
- 査読あり
- データソース
  KAKENHI-PROJECT-22300010, KAKENHI-PROJECT-23220001
[雑誌論文] Exact Flow Analysis by Higher-Order Model Checking2012
- 著者名/発表者名
  Yoshihiro Tobita, Takeshi Tsukada, Naoki Kobayashi
- 雑誌名
  
  Proceedings of FLOPS 2012, LNCS
  
  巻: 7294 ページ: 275-289
- DOI
  10.1007/978-3-642-29822-6_22
- ISBN
  9783642298219, 9783642298226
- 査読あり
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] Orderd Types for Stream Processing of Tree-Structured Date2011
- 著者名/発表者名
  Ryosuke Sato, Kohei Suenaga, Naoki Kobayashi
- 雑誌名
  
  Jornal of Information Processing
  
  巻: Vol.52 ページ: 1-14
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes2011
- 著者名/発表者名
  Naoki Kobayashi
- 雑誌名
  
  Proceedings of the 14th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2011)
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus2011
- 著者名/発表者名
  Naoki Kobayashi, C.-H.Luke Ong
- 雑誌名
  
  Logical Methods in Computer Science
  
  巻: 7(4)
- DOI
  10.2168/lmcs-7(4:9)2011
- 査読あり
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] Predicate abstraction and CEGAR for higher-order model checking2011
- 著者名/発表者名
  Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno
- 雑誌名
  
  Proceedings of the 32^<nd> ACM SIGPLAN conference on Programming language design and implementation (PLDI 2011)
  
  ページ: 222-233
- DOI
  10.1145/1993498.1993525
- 査読あり
- データソース
  KAKENHI-PROJECT-23220001
[雑誌論文] Environmental Bisimulations for Higher-Order Languages2010
- 著者名/発表者名
  Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii
- 雑誌名
  
  ACM Transactions on Programming Languages and Systems (TOPLAS)
  
  巻: Vol.33
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] Higher-Order Multi-parameter Tree Transducers and Recursion Schemes for Program Verification2010
- 著者名/発表者名
  Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno
- 雑誌名
  
  Proceedings of the 37^<th> ACM SIGPLAN-SIGACT Symposium on principles of Programming Languages (POPL 2010)
  
  ページ: 495-508
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] Verification of Tree-Processing Programs via Higher-Order Model Checking2010
- 著者名/発表者名
  Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
- 雑誌名
  
  Proceedings of the 8th Asian Symposium on Programming Languages and Systems (APLAS2010), Springer LNCS
  
  ページ: 312-327
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] Higher-Order Multi-parameter Tree Transducers and Recursion Schemes for Program Verification2010
- 著者名/発表者名
  Naoki Kobayashi, Naoshi Tabuchi and Hiroshi Unno
- 雑誌名
  
  roceedings of the 37th ACM SIGPLAN-SIGACT Symposium on principles of Programming Languages (POPL 2010)
  
  ページ: 495-508
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] ポインタのあるプログラミング言語のための資源使用法解析2010
- 著者名/発表者名
  上野慎平, 小林直樹, 海野広志
- 雑誌名
  
  情報処理学会論文誌:プログラミング
  
  巻: Vol.3 ページ: 27-42
- NAID
  110007970954
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] Untyped Recursion Schemes and Infinite Intersection Types2010
- 著者名/発表者名
  Takeshi Tsukada, Naoki Kobayashi
- 雑誌名
  
  Proceedings of the 13th International Conference on Foundations of Software Science and Computational Structures (FOSSACS'10) 6014
  
  ページ: 343-357
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification2010
- 著者名/発表者名
  Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno
- 雑誌名
  
  Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'10)
  
  ページ: 495-508
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] A hybrid type system for lock-freedom of mobile processes2010
- 著者名/発表者名
  Naoki Kobayashi, Davide Sangiorgi
- 雑誌名
  
  ACM Transactions on Programming Languages and Systems (TOPLAS) Article Number 16
  
  ページ: 49-49
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] A hybrid type system for lock-freedom of mobile processes2010
- 著者名/発表者名
  Naoki Kobayashi, Davide Sangiorgi
- 雑誌名
  
  ACM Transactions on Programming Languages and Systems (TOPLAS)
  
  巻: 16 ページ: 49-49
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs2009
- 著者名/発表者名
  Naoki Kobayashi
- 雑誌名
  
  Proceedings of the 36^<th> ACM SIGPLAN-SIGACT Symposium on principles of Programming Languages (POPL 2009)
  
  ページ: 416-428
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] Undecidable Equivalences for Basic Parallel Processes2009
- 著者名/発表者名
  Hans Huttel, Naoki Kobayashi, Takashi Suto
- 雑誌名
  
  Information and Computation 207(7)
  
  ページ: 812-819
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] Undecidable Equivalences for Basic Parallel Processes2009
- 著者名/発表者名
  Hans Huttel, Naoki Kobayashi, Takashi suto
- 雑誌名
  
  Information and Computation 207(7)巻
  
  ページ: 812-819
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs2009
- 著者名/発表者名
  Naoki Kobayashi
- 雑誌名
  
  Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL2009)
  
  ページ: 416-428
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus2009
- 著者名/発表者名
  Naoki Kobayashi, C.-H. Luke Ong
- 雑誌名
  
  Proceedings of the 36th Internatilonal Collogquium on Automata, Languages and Programming(ICALP'09) 5556(2)
  
  ページ: 223-234
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] Undecidable Equivalences for Basic Parallel Processes2009
- 著者名/発表者名
  Hans Huttel, Naoki Kobayashi and Takashi Suto
- 雑誌名
  
  Information and Computation
  
  巻: 207(7)巻ページ: 812-819
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] Model-Checking Higher-Order Functions2009
- 著者名/発表者名
  Naoki Kobayashi
- 雑誌名
  
  Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming(PPDP'09)
  
  ページ: 25-36
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] Recursion Schemes for Verification of Higher-Order Programs2009
- 著者名/発表者名
  Naoki Kobayashi, Types and Higher-Order
- 雑誌名
  
  Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on principles of Programming Languages (POPL 2009)
  
  ページ: 416-428
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] Dependent Type Inference with Interpolants2009
- 著者名/発表者名
  Hiroshi Unno, Naoki Kobayashi
- 雑誌名
  
  Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming(PPDP'09)
  
  ページ: 277-288
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] 木構造処理からストリーム処理プログラムへの変換のための部分的バッファリングの挿入2009
- 著者名/発表者名
  佐藤亮介、小林直樹
- 雑誌名
  
  情報処理学会論文誌プログラム(PRO) Vol.1-1
  
  ページ: 1-14
- NAID
  110007970840
- 査読あり
- データソース
  KAKENHI-PROJECT-19024003
[雑誌論文] A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes2009
- 著者名/発表者名
  Naoki Kobayashi, C.-H. Luke Ong
- 雑誌名
  
  Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science(LICS'09)
  
  ページ: 179-188
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] A Hybrid Type System for Lock-Freedom of Mobile Processes2008
- 著者名/発表者名
  Naoki Kobayashi, Davide Sangiorgi
- 雑誌名
  
  Proceedings of the 20th International Conference on Computer Aided Verification(CAV'08) 5123
  
  ページ: 80-93
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Translation of Tree-Processing Programs into Stream-Processing Programs Based on Ordered Linear Type2008
- 著者名/発表者名
  Koichi Kodama, Kohei Suenaga and Naoki Kobayashi
- 雑誌名
  
  Journal of Functional Programming (出版決定)
- 査読あり
- データソース
  KAKENHI-PROJECT-19024003
[雑誌論文] On-Demand Refinement of Dependent Types2008
- 著者名/発表者名
  Hiroshi Unno, Naoki Kobayashi
- 雑誌名
  
  Proceedings of the 9th International Symposium on Functional and Logic Programming(FLOPS'08) 4989
  
  ページ: 81-96
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Tree Automata for Non-Linear Arithmetic2008
- 著者名/発表者名
  Naoki Kobayashi, Hitoshi Ohsaki
- 雑誌名
  
  Proceedings of the 19th International Conference on Rewriting Techniques and Applications(RTA'08) 5117
  
  ページ: 291-305
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] A New Type System for JVM Lock Primitives2008
- 著者名/発表者名
  Futoshi Iwama, Naoki Kobayashi
- 雑誌名
  
  New Generation Computing 26(2)
  
  ページ: 125-170
- NAID
  130004548967
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] On the Complexity of Termination Inference for Processes2008
- 著者名/発表者名
  Romain Demangeon, Daniel Hirschkoff, Naoki Kobayashi and Davide Sagiorgi
- 雑誌名
  
  Proceedings of Trustworthy Global Computing 2007(TGC'07), Springer Lecture Notes in Computer Science 4912
  
  ページ: 140-155
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] A Hybrid Type System for Lock-Freedom of Mobile Processes2008
- 著者名/発表者名
  Naoki Kobayashi, Davide Sangiorgi
- 雑誌名
  
  Proceedings of the 20th International Conference on Computer Aided Verification(CAV'08) 5123
  
  ページ: 80-93
- 査読あり
- データソース
  KAKENHI-PROJECT-20240001
[雑誌論文] Linear Declassification2008
- 著者名/発表者名
  Yuta Kaneko, Naoki Kobayashi
- 雑誌名
  
  Proceedings of the 17th European Symposium on Programming(ESOP'08) 4960
  
  ページ: 224-238
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the Pi-Calculus2007
- 著者名/発表者名
  Naoki Kobayashi, Takashi Suto
- 雑誌名
  
  Proceedings of the 34th International Colloquium on Automata, Languages and Programming(ICALP'07) 4596
  
  ページ: 740-751
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] An Algorithm to Decide Conformance of Resource Usage to Specification for Resource Usage Verification2007
- 著者名/発表者名
  Futoshi Iwama, Atsushi Igarashi, Naoki Kobayashi
- 雑誌名
  
  IPSJ Transactions on Programming 48(SIG 4(PRO 32))
  
  ページ: 48-61
- NAID
  110006242945
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Introduction of Channel Usage Declaration for Concurrent Programming Languages2007
- 著者名/発表者名
  Takashi Suto, Naoki Kobayashi
- 雑誌名
  
  IPSJ Transactions on Programming 48(SIG 10(PRO 33))
  
  ページ: 101-113
- NAID
  110006291060
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] 並行プログラミング言語へのチャネル使用法宣言の導入2007
- 著者名/発表者名
  須藤崇, 小林直樹
- 雑誌名
  
  情報処理学会論文誌:プログラミング 48(SIG10(PRO33))
  
  ページ: 101-113
- NAID
  110006291060
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts2007
- 著者名/発表者名
  Kohei Suenaga, Naoki Kobayashi
- 雑誌名
  
  Proceedings of the 16th European Symposium on Programming(ESOP'07) 4421
  
  ページ: 490-504
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] XMLのためのストリーム処理プログラム生成器X-P2007
- 著者名/発表者名
  佐藤修二, 末永幸平, 小林直樹
- 雑誌名
  
  PPL2007 論文集
  
  ページ: 218-218
- データソース
  KAKENHI-PROJECT-18049002
[雑誌論文] Type-Based Verification of Correspondence Assertions for Communication Protocols2007
- 著者名/発表者名
  Daisuke Kikuchi and Naoki Kobayashi
- 雑誌名
  
  Proceedings of the 5th Asian Symposium on Programming Languages and Systems(APLAS'07), Springer Lecture Notes in Computer Science 4807
  
  ページ: 191-205
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Environmental Bisimulations for Higher-Order Languages2007
- 著者名/発表者名
  Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii
- 雑誌名
  
  Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science(LICS'07)
  
  ページ: 293-302
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Type-Based Verification of Correspondence Assertions for Communication Protocols2007
- 著者名/発表者名
  Daisuke Kikuchi, Naoki Kobayashi
- 雑誌名
  
  Proceedings of the 5th ASIAN Symposium on Programming Languages and Systems(APLAS'07) 4807
  
  ページ: 191-205
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the Pi-Calculus2007
- 著者名/発表者名
  Naoki Kobayashi and Takashi Suto
- 雑誌名
  
  Proceedings of the 34th International Colloquium on Automata, Languages and Programming(ICALP'07) 4596
  
  ページ: 740-751
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] 計算資源使用法検証における計算資源の仕様と実際の使用法の間の適合性検証アルゴリズム2007
- 著者名/発表者名
  岩間太, 五十嵐淳, 小林直樹
- 雑誌名
  
  情報処理学会プログラミング研究会論文誌 48・SIG4
  
  ページ: 48-61
- データソース
  KAKENHI-PROJECT-16650004
[雑誌論文] Environmental Bisimulations for Higher-Order Languages2007
- 著者名/発表者名
  Davide Sangiorgi, Naoki kobayashi, Eijiro Sumii
- 雑誌名
  
  Proceedings of IEEE Symposium on Logic in Computer Science (LICS 2007) (出版決定)
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] 計算資源使用法検証における計算資源の仕様と実際の使用法の間の適合性検証アルゴリズム2007
- 著者名/発表者名
  岩間太, 五十嵐淳, 小林直樹
- 雑誌名
  
  情報処理学会プログラミング研究会論文誌 48・SIG4
  
  ページ: 48-61
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts2007
- 著者名/発表者名
  Kohei Suenaga, Naoki Kobayashi
- 雑誌名
  
  Proceedings of 16th European Symposium on Programming (ESOP'07), Springer Lecture Notes in Computer Science 4421
  
  ページ: 490-504
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] On the Complexity of Termination Inference for Processes2007
- 著者名/発表者名
  Romain Demangeon, Daniel Hirschkoff, Naoki Kobayashi, Davide Sangiorgi
- 雑誌名
  
  Proceedings of Trustworthy Global Computing(TGC'07) 4912
  
  ページ: 140-155
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] 計算資源使用法検証における計算資源の仕様と実際の使用法の間の適合性検証アルゴリズム2007
- 著者名/発表者名
  岩間太, 五十嵐淳, 小林直樹
- 雑誌名
  
  情報処理学会論文誌:プログラミング 48(SIG4(PRO32))
  
  ページ: 48-61
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Resource usage analysis for the pi-calculus2006
- 著者名/発表者名
  Naoki Kobayashi, Kohei Suenaga, Lucian Wischik
- 雑誌名
  
  Verification, Model Checking, and Abstract Interpretation (Proceedings of UMCAI' 06) 3855
  
  ページ: 298-312
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Resource Usage Analysis for the Pi-Calculus2006
- 著者名/発表者名
  Naoki Kobayashi, Kohei Suenaga, Lucian Wischik
- 雑誌名
  
  Logical Methods in Computer Science 22・2:3
  
  ページ: 1-42
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Resource usage analysis for the pi-calculus2006
- 著者名/発表者名
  Naoki Kobayashi, Kohei Suenaga, Lucian Wischik
- 雑誌名
  
  Verification, Model Checking, and Abstract Interpretation (Proceedings of VMCAI'06) 3855
  
  ページ: 298-312
- データソース
  KAKENHI-PROJECT-16650004
[雑誌論文] A New Type System for Deadlock-Free Processes2006
- 著者名/発表者名
  Naoki Kobayashi
- 雑誌名
  
  Proceedings of CONCUR 2006, Springer Lecture Notes in Computer Science 4137
  
  ページ: 233-247
- データソース
  KAKENHI-PROJECT-16650004
[雑誌論文] Resource usage analysis for a functional language with exceptions2006
- 著者名/発表者名
  Futoshi Iwama, Atsushi Igarashi, Naoki Kobayashi
- 雑誌名
  
  Proceedings of ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program Manipulation (PEPM 2006)
  
  ページ: 38-47
- データソース
  KAKENHI-PROJECT-16650004
[雑誌論文] Combining Type-Based Analysis and Model Checking for Finding Counterexamples against Non-Interference2006
- 著者名/発表者名
  Hiroshi Unno, Naoki Kobayashi, Akinori Yonezawa
- 雑誌名
  
  Proceedings of ACM SIGPLAN Workshop on Programming Languages and Analysis for Security(PLAS'06)
  
  ページ: 17-26
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Combining Type-Based Analysis and Model Checking for Finding Counterexamples against Non-Interference2006
- 著者名/発表者名
  Hiroshi Unno, Naoki Kobayashi, Akinori Yonezawa
- 雑誌名
  
  Proceedings of ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS 2006)
  
  ページ: 17-26
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Resource Usage Analysis for a Functional Language with Exceptions2006
- 著者名/発表者名
  Futoshi Iwama, Atsushi Igarashi, Naoki Kobayashi
- 雑誌名
  
  Proceedings of ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program Manipulation(PEPM'06)
  
  ページ: 38-47
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Resource usage analysis for a functional language with exceptions2006
- 著者名/発表者名
  Futoshi Iwama, Atsushi Igarashi, Naoki Kobayashi
- 雑誌名
  
  Proceedings of ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program Manipulation (PEPM 2006)
  
  ページ: 38-47
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] A New Type System for Deadlock-Free Processes2006
- 著者名/発表者名
  Naoki Kobayashi
- 雑誌名
  
  Proceedings of the 17th International Conference on Concurrency Theory(CONCUR'06) 4137
  
  ページ: 233-247
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Extension of type-based approach to generation of stream-processing programs by automatic insertion of buffering primitives2006
- 著者名/発表者名
  Kohei Suenaga, Naoki Kobayashi, Akinori Yonezawa
- 雑誌名
  
  Proceedings of LOPSTER 2005 3901
  
  ページ: 98-114
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] A New Type System for Deadlock-Free Processes2006
- 著者名/発表者名
  Naoki Kobayashi
- 雑誌名
  
  Proceedings of CONCUR 2006, Springer Lecture Notes in Computer Science 4137
  
  ページ: 233-247
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Resource Usage Analysis for the Pi-Calculus2006
- 著者名/発表者名
  Naoki Kobayashi, Kohei Suenaga, Lucian Wischik
- 雑誌名
  
  Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation(VMCAI'06) 3855
  
  ページ: 298-312
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] A New Type System for Deadlock-Free Processes2006
- 著者名/発表者名
  小林直樹
- 雑誌名
  
  Proceedings of the 17th International Conference on Concurrency Theory(CONCUR'06) 4137
  
  ページ: 233-247
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Combining Type-Based Analysis and Model Checking for Finding Counterexamples against Non-Interference2006
- 著者名/発表者名
  Hiroshi Unno, Naoki Kobayashi, Akinori Yonezawa
- 雑誌名
  
  Proceedings of ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS 2006)
  
  ページ: 17-26
- データソース
  KAKENHI-PROJECT-16650004
[雑誌論文] Resource Usage Analysis for the Pi-Calculus2006
- 著者名/発表者名
  Naoki Kobayashi, Kohei Suenaga, Lucian Wischik
- 雑誌名
  
  Logical Methods in Computer Science 2(3:4)
  
  ページ: 1-42
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Resource Usage Analysis2005
- 著者名/発表者名
  Atsushi Igarashi, Naoki Kobayashi
- 雑誌名
  
  ACM Transactions on Programming Languages and Systems 27・2(出版予定)
- データソース
  KAKENHI-PROJECT-16650004
[雑誌論文] Verification of Concurrent Programs using the Coq Proof Assistant : a Case Study2005
- 著者名/発表者名
  R.Affeldt, N.Kobayashi, A.Yonezawa
- 雑誌名
  
  IPSJ Transactions on Programming 46・SIG1
  
  ページ: 110-120
- NAID
  130000022400
- データソース
  KAKENHI-PROJECT-14702063
[雑誌論文] Type-Based Information Flow Analysis for the Pi-Calculus2005
- 著者名/発表者名
  小林直樹
- 雑誌名
  
  Acta Informatica 42(4-5)
  
  ページ: 291-347
- 説明
  「研究成果報告書概要(和文)」より
- 査読あり
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] 例外機構を備えた言語のための資源使用法解析2005
- 著者名/発表者名
  岩間太, 五十嵐淳, 小林直樹
- 雑誌名
  
  第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集 (印刷中)
- データソース
  KAKENHI-PROJECT-16650004
[雑誌論文] Type-Based Information Flow Analysis for the Pi-Calculus2005
- 著者名/発表者名
  Naoki Kobayashi
- 雑誌名
  
  Acta Informatica 42(4-5)
  
  ページ: 291-347
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Type-based information flow analysis for the pi-calculus2005
- 著者名/発表者名
  Naoki Kobayashi
- 雑誌名
  
  Acta Informatica 41・4-5
  
  ページ: 291-347
- データソース
  KAKENHI-PROJECT-17300003
[雑誌論文] Resource Usage Analysis2005
- 著者名/発表者名
  Atsushi Igarashi, Naoki Kobayashi
- 雑誌名
  
  ACM TOPLAS 27・2(出版予定)
- データソース
  KAKENHI-PROJECT-14702063
[雑誌論文] A Coq Library for Verification of Concurrent Programs2004
- 著者名/発表者名
  Reynald Affeldt, Naoki Kobayashi
- 雑誌名
  
  Proceedings of LFM 2004
  
  ページ: 66-83
- データソース
  KAKENHI-PROJECT-14702063
[雑誌論文] Translation of Tree-Processing Programs into Stream-Processing Programs Based on Ordered Linear Type2004
- 著者名/発表者名
  K.Kodama, K.Suenaga, N.Kobayashi
- 雑誌名
  
  Proceedings of APLAS'04 (Springer LNCS) 3302
  
  ページ: 41-56
- データソース
  KAKENHI-PROJECT-14702063
[雑誌論文] Region-Based Memory Management for a Dynamically-Typed Language2004
- 著者名/発表者名
  A.Nagata, N.Kobayashi, A.Yonezawa
- 雑誌名
  
  Proceedings of APLAS' 04, Springer LNCS 3302
  
  ページ: 229-245
- NAID
  130004638815
- データソース
  KAKENHI-PROJECT-16650004
[雑誌論文] A Generic Type System for the Pi-Calculus2004
- 著者名/発表者名
  Atsushi Igarashi, Naoki Kobayashi
- 雑誌名
  
  Theoretical Computer Science (Elsevier Science Publishers) 311(1-3)
  
  ページ: 121-163
- データソース
  KAKENHI-PROJECT-14702063
[雑誌論文] Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes2004
- 著者名/発表者名
  Reynald Affeldt, Naoki Kobayashi
- 雑誌名
  
  Proceedings of 11^<th> International Workshop on Expressiveness in Concurrency (EXPRESS 2004)
  
  ページ: 113-127
- データソース
  KAKENHI-PROJECT-16650004
[学会発表] On Type-Based Techniques for Program Manipulation2022
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2022)
- 招待講演 / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-20H05703
[学会発表] An Overview of the HFL Model Checking Project2021
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  8th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2021)
- 招待講演 / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-20H05703
[学会発表] 10 Years of the Higher-Order Model Checking Project2019
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  21st International Symposium on Principles and Practice of Programming Languages (PPDP 2019)
- 招待講演 / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15H05706
[学会発表] On Two Kinds of Higher-Order Model Checking and Higher-Order Program Verification2018
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  HOR 2018
- 招待講演 / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15H05706
[学会発表] On Two Kinds of Higher-Order Model Checking and Higher-Order Program Verification2018
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  9th Workshop on Higher-Order Rewriting
- 招待講演 / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15H05706
[学会発表] Program Verification Based on Higher-Order Model Checking2016
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  Dagstuhl seminar on Language Based Verification Tools for Functional Programs
- 発表場所
  Schloss Dagstuhl (ドイツ、Wadern）
- 年月日
  2016-03-30
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15H05706
[学会発表] On Two Higher-Order Extensions of Model Checking2016
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  FTSCS 2016
- 招待講演 / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15H05706
[学会発表] Higher-order model checking and program verification2015
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  IFIP WG 2.11 meeting
- 発表場所
  Imperial College（イギリス、London）
- 年月日
  2015-11-09
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15H05706
[学会発表] 参照を備えた多段階計算のための多相的型システム2015
- 著者名/発表者名
  小林恵，五十嵐淳
- 学会等名
  日本ソフトウェア科学会第32回大会
- 発表場所
  早稲田大学理工学部
- 年月日
  2015-09-11
- データソース
  KAKENHI-PROJECT-25280025
[学会発表] Program verification via higher-order model checking2015
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  IFIP WG 2.2 meeting
- 発表場所
  Institute for Advanced Studies Lucca（イタリア、Lucca）
- 年月日
  2015-09-21
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15H05706
[学会発表] RePair流高階圧縮アルゴリズムの最適化2014
- 著者名/発表者名
  武田広太郎、小林直樹、松田一孝
- 学会等名
  日本ソフトウェア科学会大会
- 発表場所
  名古屋大学（愛知県名古屋市）
- 年月日
  2014-09-09
- データソース
  KAKENHI-PROJECT-23220001
[学会発表] Program Certification by Higher-Order Model Checking2012
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  Certified Programs and Proofs - Second International Conference, CPP 2012
- 発表場所
  京都国際交流会館（京都府）
- 招待講演
- データソース
  KAKENHI-PROJECT-23220001
[学会発表] Higher-Order Model Checking : From Theory to Practice2011
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS 2011)
- 発表場所
  カナダ・トロント(招待講演)
- 年月日
  2011-06-23
- データソース
  KAKENHI-PROJECT-23220001
[学会発表] Towards a software model checker for ML2011
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  ACM SIGPLAN Workshop on ML 2011
- 発表場所
  日本・東京(招待講演)
- 年月日
  2011-09-18
- データソース
  KAKENHI-PROJECT-23220001
[学会発表] Higher-order model checking for program verification2010
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  Workshop on automata and logic for data manipulating programs
- 発表場所
  フランスパリ
- 年月日
  2010-12-07
- データソース
  KAKENHI-PROJECT-20240001
[学会発表] Types and Recursion Schemes for Higher-Order Program Verification2010
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  Workshop on Higher-Order Recursion Schemes and Pushdown Automata
- 発表場所
  フランスパリ,招待講演.
- 年月日
  2010-03-11
- データソース
  KAKENHI-PROJECT-20240001
[学会発表] Model-Checking Higher-Order Programs2010
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  Daghstul seminar on Game Semantics and Program Verification
- 発表場所
  ドイツ・ダーグストゥール
- 年月日
  2010-06-21
- データソース
  KAKENHI-PROJECT-20240001
[学会発表] Higher-order model checking for program verification2010
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  Workshop on automata and logic for data manipulating programs
- 発表場所
  フランス・パリ
- 年月日
  2010-12-07
- データソース
  KAKENHI-PROJECT-20240001
[学会発表] Types and Recursion Schemes for Higher-Order Program Verification2010
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  Workshop on Higher-Order Recursion Schemes and Pushdown Automata
- 発表場所
  フランスパリ
- 年月日
  2010-03-11
- データソース
  KAKENHI-PROJECT-20240001
[学会発表] Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification2010
- 著者名/発表者名
  Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno
- 学会等名
  日本ソフトウェア科学会第27回特別講演
- 発表場所
  日本・東京
- 年月日
  2010-09-13
- データソース
  KAKENHI-PROJECT-20240001
[学会発表] Higher-order model checking for program verification2010
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  Workshop on automata and logic for data manipulating programs
- 発表場所
  フランスパリ,招待講演.
- 年月日
  2010-12-07
- データソース
  KAKENHI-PROJECT-20240001
[学会発表] Types and Recursion Schemes for Higher-Order Program Verification2009
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  the 7th Asian Symposium on Programming Languages and Systems (APLAS 2009)
- 発表場所
  韓国ソウル
- 年月日
  2009-12-16
- データソース
  KAKENHI-PROJECT-20240001
[学会発表] Higher-Order Program Verification and Language-Based Security2009
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  13th Annual Asian Computing Science Conference (ASIAN'09)
- 発表場所
  韓国・ソウル
- 年月日
  2009-12-16
- データソース
  KAKENHI-PROJECT-20240001
[学会発表] Ordered Types for Stream Processing of Tree-Structured Data2009
- 著者名/発表者名
  Ryosuke Sato, Kohei Suenaga and Naoki Kobayashi
- 学会等名
  Programming Language Techniques for XML (PLAN-X 2009)
- 発表場所
  アメリカ合衆国ジョージア州
- 年月日
  2009-01-24
- データソース
  KAKENHI-PROJECT-19024003
[学会発表] Types and Recursion Schemes for Higher-Order Program Verification2009
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  7th Asian Symposium on Programming Languages and Systems (APLAS'09)
- 発表場所
  韓国・ソウル
- 年月日
  2009-12-16
- データソース
  KAKENHI-PROJECT-20240001
[学会発表] Higher-Order Program Verification and Language-Based Security2009
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  the 13th Annual Asian Computing Science Conference (ASIAN 2009)
- 発表場所
  韓国ソウル
- 年月日
  2009-12-16
- データソース
  KAKENHI-PROJECT-20240001
[学会発表] Higher-Order Program Verification and Language-Based Security2009
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  the 13th Annual Asian Computing Science Conference (ASIAN 2009)
- 発表場所
  韓国ソウル,招待講演.
- 年月日
  2009-12-16
- データソース
  KAKENHI-PROJECT-20240001
[学会発表] Types and Recursion Schemes for Higher-Order Program Verification2009
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  the 7th Asian Symposium on Programming Languages and Systems (APLAS 2009)
- 発表場所
  韓国ソウル,招待講演.
- 年月日
  2009-12-16
- データソース
  KAKENHI-PROJECT-20240001
[学会発表] Substructural Type Systems for Program Analysis2008
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  Proceedings of the 9th International Symposium on Functional and Logic Programming(FLOPS'08)
- 発表場所
  三重県伊勢市
- 年月日
  2008-04-16
- 説明
  「研究成果報告書概要(和文)」より
- データソース
  KAKENHI-PROJECT-17300003
[学会発表] Substructural Type Systems for Program Analysis2008
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  Proceedings of the 9th International Symposium on Functional and Logic Programming(FLOPS'08)
- 発表場所
  Ise, Mie
- 年月日
  2008-04-16
- 説明
  「研究成果報告書概要(欧文)」より
- データソース
  KAKENHI-PROJECT-17300003
[学会発表] Substructural Type Systems for Program Analysis2008
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  The 9th International Symposium on Functional and Logic Programming(FLOPS'08)
- 発表場所
  三重県伊勢市
- 年月日
  2008-04-16
- データソース
  KAKENHI-PROJECT-20240001
[学会発表] Substructural Type Systems for Program Analysis2008
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  The 9th International Symposium on Functional and Logic Programming (FLOPS 2008)
- 発表場所
  三重県伊勢市
- 年月日
  2008-04-16
- データソース
  KAKENHI-PROJECT-20240001
[学会発表] 木構造処理からストリーム処理プログラムへの変換のための部分的バッファリングの挿入2008
- 著者名/発表者名
  佐藤亮介、小林直樹
- 学会等名
  情報処理学会第67回プログラミング研究会
- 発表場所
  東北大学電気通信研究所
- 年月日
  2008-01-24
- データソース
  KAKENHI-PROJECT-19024003
[学会発表] Substructural Type Systems for Program Analysis2008
- 著者名/発表者名
  Naoki Kobayashi
- 学会等名
  The 9th International Symposium on Functional and Logic Programming (FLOPS 2008)
- 発表場所
  三重県伊勢市,招待講演.
- 年月日
  2008-04-16
- データソース
  KAKENHI-PROJECT-20240001
[学会発表] 文脈依存資源使用解析のための型システム2008
- 著者名/発表者名
  仲井間達也、五十嵐淳、小林直樹
- 学会等名
  第10回プログラミングおよびプログラミング言語ワークショップ(PPL'08)
- 発表場所
  仙台市
- 年月日
  2008-03-06
- データソース
  KAKENHI-PROJECT-17300003
[学会発表] 型エラースライシングによるデッドロックの原因個所の特定2008
- 著者名/発表者名
  飯村枝里、末永幸平、小林直樹
- 学会等名
  情報処理学会第68回プログラミング研究会
- 発表場所
  日本IBM(株)東京基礎研究所
- 年月日
  2008-03-17
- データソース
  KAKENHI-PROJECT-17300003
[学会発表] 高階木変換器の自動検証のための反例発見と抽象化改良
- 著者名/発表者名
  松本雄磨、小林直樹、海野広志
- 学会等名
  第16回プログラミングおよびプログラミング言語ワークショップ(PPL 2014)
- 発表場所
  阿蘇の司ビラパークホテル(熊本県阿蘇市)
- 年月日
  2014-03-05 – 2014-03-07
- データソース
  KAKENHI-PROJECT-23220001

1. 五十嵐淳 (40323456)

共同の研究課題数: 10件

共同の研究成果数: 13件
2. 住井英二郎 (00333550)

共同の研究課題数: 6件

共同の研究成果数: 3件
3. 米澤明憲 (00133116)

共同の研究課題数: 5件

共同の研究成果数: 0件
4. 海野広志 (80569575)

共同の研究課題数: 4件

共同の研究成果数: 8件
5. 岡田光弘 (30224025)

共同の研究課題数: 3件

共同の研究成果数: 0件
6. 田浦健次朗 (90282714)

共同の研究課題数: 3件

共同の研究成果数: 0件
7. 寺内多智弘 (70447150)

共同の研究課題数: 3件

共同の研究成果数: 3件
8. 松岡聡 (20221583)

共同の研究課題数: 3件

共同の研究成果数: 0件
9. 佐藤亮介 (10804677)

共同の研究課題数: 3件

共同の研究成果数: 18件
10. 佐藤雅彦 (20027387)

共同の研究課題数: 2件

共同の研究成果数: 0件
11. 松田一孝 (10583627)

共同の研究課題数: 2件

共同の研究成果数: 2件
12. 篠原歩 (00226151)

共同の研究課題数: 2件

共同の研究成果数: 4件
13. 増原英彦 (40280937)

共同の研究課題数: 2件

共同の研究成果数: 0件
14. 米崎直樹 (00126286)

共同の研究課題数: 2件

共同の研究成果数: 0件
15. 渡部卓雄 (20222408)

共同の研究課題数: 1件

共同の研究成果数: 0件
16. 照井一成 (70353422)

共同の研究課題数: 1件

共同の研究成果数: 0件
17. 田村直之 (60207248)

共同の研究課題数: 1件

共同の研究成果数: 0件
18. 二木厚吉 (50251971)

共同の研究課題数: 1件

共同の研究成果数: 0件
19. 萩谷昌己 (30156252)

共同の研究課題数: 1件

共同の研究成果数: 0件
20. 西澤弘毅 (60455433)

共同の研究課題数: 1件

共同の研究成果数: 0件
21. 加藤和彦 (90224493)

共同の研究課題数: 1件

共同の研究成果数: 0件
22. 林晋 (40156443)

共同の研究課題数: 1件

共同の研究成果数: 0件
23. 外山芳人 (00251968)

共同の研究課題数: 1件

共同の研究成果数: 0件
24. 桜井貴文 (60183373)

共同の研究課題数: 1件

共同の研究成果数: 0件
25. 塚田武志 (50758951)

共同の研究課題数: 1件

共同の研究成果数: 10件
26. 吉仲亮 (80466424)

共同の研究課題数: 1件

共同の研究成果数: 10件
27. 関山太朗 (80828476)

共同の研究課題数: 1件

共同の研究成果数: 1件
28. 佐藤一誠 (90610155)

共同の研究課題数: 1件

共同の研究成果数: 10件
29. 登内敏夫

共同の研究課題数: 1件

共同の研究成果数: 0件
30. 遠藤敏夫

共同の研究課題数: 1件

共同の研究成果数: 0件
31. 山本泰宇

共同の研究課題数: 1件

共同の研究成果数: 0件
32. 大山恵弘

共同の研究課題数: 1件

共同の研究成果数: 0件
33. 浅田和之

共同の研究課題数: 0件

共同の研究成果数: 1件

小林 直樹 Kobayashi Naoki

研究課題

研究成果

共同研究者

検証指向プログラミング言語の設計と実装研究代表者

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

高階不動点論理に基づくプログラム検証研究代表者

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

AI時代を見据えたプログラム検証技術研究代表者

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

高階モデル検査の深化と発展研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

クラス理論に基づく自己拡張可能なソフトウェア検証体系の構築

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

高階モデル検査とその応用研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

ソフトウェアの安全性向上のための型理論の深化と応用研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

順序付き線形型に基づく安全かつ高速な大規模データ処理の実現研究代表者

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

順序付き線形型に基づく安全かつ高速な大規模データ処理の実現研究代表者

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

ソフトウェアの安全性向上のための型理論研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

型システムとモデル検査の融合によるソフトウェア検証研究代表者

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

日米科学協力事業「ソフトウェア検証の論理的方法」更新のための企画研究

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

充実期を迎えた線形論理の進化とその応用に関する研究

研究代表者

研究期間 (年度)

研究種目

小林直樹 Kobayashi Naoki