東京大学の小林と申します。
以下の条件で、研究員の募集を致します。お近くに興味のありそうな方が いらっしゃいましたらご紹介いただければ幸いです。
過去に高階モデル検査のプロジェクトについて研究員の募集をしましたが、 今回は高階モデル検査に限らないプログラム検証手法全般、および機械学習との 融合・応用も含む、広めのプロジェクト設定になっております。 ご本人の能力・経験次第では特別な審査を経て特任助教または特任講師での採用 または途中での職位変更も可能です。
小林直樹 東京大学大学院情報理工学系研究科コンピュータ科学専攻
================ 公募
職名：特任研究員，特任助教，または特任講師 （ただし、特任助教および特任講師は、教育能力等についての審査もあり）
着任時期：2021年11月から2022年4月の間（数ヵ月の前後は応相談）
任期：当初2年、業績評価を経て最長2025年3月まで延長可能
勤務場所：東京大学大学院情報理工学系研究科コンピュータ科学専攻 （ただし、本人の希望によっては，共同研究者の所属である京都大学への配置も可能）
給与：月額38-55万円 （大学の規定および本人の実績による．詳細は応相談.）
プロジェクト名：AI時代を見据えたプログラム検証技術（科研費基盤研究S 20H05703）
職務内容： 高階モデル検査をはじめとするプログラム検証手法、機械学習技術のプログラム検証への応用、 および機械学習を組み込んだシステムの検証等の研究に従事。 特任助教、および特任講師の場合は研究指導の補助など教育等の業務にも従事。
条件： - 着任時に博士号を取得していること
- 理論計算機科学全般または機械学習技術に明るいこと．
- 以下の中の１つ以上のトピックに詳しくプログラミング能力が高いか、 ２つ以上のトピックに詳しいこと
モデル検査（特にソフトウェアモデル検査） 型システム プログラム意味論 プログラム解析・検証・変換 オートマトンと形式言語理論 自動定理証明 計算量理論 機械学習（ニューラルネット、強化学習、形式言語の学習理論など）
応募方法： 2021年8月31日までに、小林（[email protected])まで、CV(略歴、 業績等を記載したもの）および抱負（1頁程度）、照会先情報（2名程度）をお送りください。
問い合わせ先： [email protected]
参考資料等： 高階モデル検査およびそれに基づくプログラム検証の概要については以下の招待講演論文・講演を ご覧ください * Naoki Kobayashi, 10 Years of the Higher-Order Model Checking Project (Extended Abstract). PPDP 2019: 2:1-2:2 https://www-kb.is.s.u-tokyo.ac.jp/~koba/papers/ppdp19.pdf (talk: https://www.youtube.com/watch?v=smJhjuv9RYw )
* Naoki Kobayashi, An Overview of the HFL Model Checking Project, HCVS 2021 https://www-kb.is.s.u-tokyo.ac.jp/~koba/papers/hcvs21.pdf (talk: https://www.youtube.com/watch?v=lOY0Xw8i3zY )
機械学習とプログラム検証・合成分野の融合についての研究はまだ始めたばかりですが 最初の結果をまとめた以下の論文をご覧いただければ目指している方向がわかっていただけると 思います
* Naoki Kobayashi, Taro Sekiyama, Issei Sato, and Hiroshi Unno, Toward Neural-Network-Guided Program Synthesis and Verification. To appear in Proceedings of SAS 2021. (A preliminary version: https://arxiv.org/abs/2103.09414 ) =====================