小林直樹

コバヤシナオキ | Kobayashi Naoki

所属機関・部署：
職名：教授
ホームページURL (1件)： http://www-kb.is.s.u-tokyo.ac.jp/~koba/

研究分野 (2件)：ソフトウェア , 情報学基礎論

研究キーワード (4件)：プログラミング言語 , 型システム , 高階モデル検査 , プログラム検証

競争的資金等の研究課題 (6件)：

全件表示

論文 (165件)：

Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, Takeshi Tsukada. HFL(Z) Validity Checking for Automated Program Verification. Proc. ACM Program. Lang. 2023. 7. POPL. 154-184
Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi. On Higher-Order Reachability Games Vs May Reachability. Proceedings of RP 2022. 2022. 108-124
Ryoya Mukai, Naoki Kobayashi, Ryosuke Sato. Parameterized Recursive Refinement Types for Automated Program Verification. Proceedings of SAS 2022. 2022. 397-421
Mahmudul Faisal Al Ameen, Naoki Kobayashi, Ryosuke Sato. Asynchronous Unfold/Fold Transformation for Fixpoint Logic. Functional and Logic Programming - 16th International Symposium(FLOPS). 2022. 39-56
Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato. Symbolic Automatic Relations and Their Applications to SMT and CHC Solving. Static Analysis - 28th International Symposium(SAS). 2021. 405-428

MISC (7件)：

Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi. Refinement Type Checking via Assertion Checking. 情報処理学会論文誌プログラミング(PRO). 2015. 8. 3
矢口和也, 小林直樹, 篠原歩. 高階圧縮の高速化と効率の良い符号化 (コンピュテーション). 電子情報通信学会技術研究報告 = IEICE technical report : 信学技報. 2013. 113. 252. 13-20
Ryosuke Sato, Kohei Suenaga, Naoki Kobayashi. Ordered Types for Stream Processing of Tree-Structured Data. 情報処理学会論文誌. 2011. 52. 2. 766-779
飯村枝里, 小林直樹, 末永幸平. 型エラースライシングによるデッドロックの原因特定. 情報処理学会論文誌プログラミング(PRO). 2008. 1. 2. 71-84
佐藤亮介, 小林直樹. 木構造処理からストリーム処理プログラムへの変換のための部分的バッファリングの挿入. 情報処理学会論文誌プログラミング(PRO). 2008. 1. 1. 1-14

書籍 (1件)：

講演・口頭発表等 (10件)：

10 Years of the Higher-Order Model Checking Project
(21st International Symposium on Principles and Practice of Programming Languages (PPDP 2019) 2019)
On Two Kinds of Higher-Order Model Checking and Higher-Order Program Verification
(HOR 2018 2018)
On Two Higher-Order Extensions of Model Checking
(FTSCS 2016 2016)
Program Certification by Higher-Order Model Checking
(CPP 2012 2012)
Towards a software model checker for ML
(ML Workshop 2011)

学歴 (2件)：

学位 (1件)：

経歴 (5件)：

委員歴 (18件)：

全件表示

受賞 (7件)：

2014 - ETAPS 2014 Best Paper Award (EATCS Best Paper Award) Unsafe Order-2 Tree Languages Are Context-Sensitive
2010 - 日本ソフトウェア科学会 2010年度基礎研究賞高階関数型プログラムの検証に関する研究
2009 - 第5回日本学術振興会賞
2008 - RTA 2008 Best Paper Award Tree Automata for Non-linear Arithmetic
2006 - 文部科学大臣表彰若手科学者賞

全件表示

※　J-GLOBALの研究者情報は、researchmapの登録情報に基づき表示しています。登録・更新については、こちらをご覧ください。

小林 直樹