| 取得学位 | 博士（情報科学）（北海道大学） |
|---|---|
| 担当科目 | 計算機言語学Ⅰ・Ⅱ、計算機実習Ⅰ、情報工学基礎Ⅱ、オペレーティングシステム、卒業研究 |
| 専門分野 | 情報工学（ソフトウェア工学） |
| 研究テーマ | ソフトウェアが期待される性質を持つことを数学的・論理的に厳密に証明する「形式的検証」の技術をより使いやすいものとすることを目指し、その基礎となるコンピュータによる定理自動証明技術について研究しています。また最近は、ソフトウェアがどのような性質を持つか自体も自動的に見つける「定理・仕様の自動発見」の分野にも取り組んでいます。 |
| キーワード | 定理自動証明、形式的検証、項書換え系、関数型プログラミング |
| 教育・研究への 取り組み | 講義では、問題の解き方を覚えてもらうことより、その解き方が発明されるに至った過程・根本にあるアイデアをじっくり理解してもらうことを重視しています。研究では、定理自動証明の分野における基礎的・一般的な成果を得ることを目指しつつ、同時にそれが現実的なソフトウェア検証への応用においても役立つものとなるよう、研究課題や問題設定を考えるようにしています。 |
| 教育研究紹介 | コンピュータを用いた論理的な推論の自動化（定理自動証明）と、そのソフトウェア検証への応用 |
| 趣味 | 散歩、ペンシルパズル、アコースティックギター |
| おすすめの作品 | （本）広中平祐「学問の発見」 |
受験生へメッセージ
情報工学の分野では、コンピュータさえあれば興味のあるシステムを自分で設計し、組み立て、動かし、改良していく過程全体の楽しみが味わえます。大学ではそのための基礎となるプログラミング力、数学的・論理的思考力、文献を読む力などをしっかり身に着けてもらい、ソフトウェアという形で自分のアイデアを実現させる醍醐味を存分に体験してもらえればと思います。
