情報科学科TOP > 教員紹介
ページの本文を印刷

木下 佳樹(きのした よしき)

 
職名 教授・理学博士
担当科目 情報科学実験Ⅱ
情報ゼミナール
数理・情報科学の世界
総合理学研究Ⅰ・Ⅱ
卒業研究Ⅰ・Ⅱ
ソフトウェア基礎
ソフトウェアデザイン論
プログラミング演習Ⅰ・Ⅱ
プログラミングII
プログラミングII演習
輪講Ⅰ・Ⅱ
専門分野 プログラミング科学。算譜意味論(プログラム意味論)、算譜検証論(プログラム検証論)、妥当性確認論(theory of validation)
ホームページ 木下佳樹研究室
「神大の先生」木下佳樹のページ
「神大の研究室」 木下 佳樹 研究室
 

主要著書、論文

* Y.Kinoshita and J.A.Power. Category Theoretic Structure of Setoids, accepted for publication, Theoretical Computer Science, Elsevier.
* Y.Kinoshita and M.Takeyama. Assurance Case as a Proof in a Theory, In C.Dale and T.Anderson (eds.), Assuring the Safety of Systems: Proceedings of the Twenty-first Safety-critical Systems Symposium, Bristol, Uk, 5-7th February 2013, Safety Critical Systems Club, ISBN-13: 978-1481018647, 2013.

略歴

1956昭和31年大阪生まれ。東京大学理学部情報科学科卒業後テキサスインスツルメンツ勤務などをへて1989平成元年から2001年平成13年まで電子技術総合研究所、同年機構改変により産業技術総合研究所(産総研)勤務となり2013年まで在勤。2013年より現職。この間1992年より一年間エディンバラ大学LFCS客員研究員として在外研究、2004年より2010年まで産総研システム検証研究センター長。2010年より2012年まで奈良先端科学技術大学院大学情報科学研究科プログラミング科学連携講座教授。その他千葉大学理学部、東京大学大学院理学系研究科、筑波大学数学系、神戸大学工学部などで非常勤講師。

研究テーマ

○プログラミングの科学を研究します。
• プログラムとは何か?(算譜意味論)
プログラムを研究します。
• プログラムが正しいとは?(算譜検証論)
プログラムが、明確に記された性質を持つことを、論理的に証明する手法を研究します。
• システムが妥当だとは?(妥当性確認論)
システムの利用者からの要求は明確に記されているとは限りません。一定条件のもとで、関係者からの要求に応えていることの確認手法を研究します。
• システムへの要求の分析手法(要求分析論)
システムにどんな性質を期待するのかを分析し、明確に記すための手法を研究します。

研究内容について

本研究室では、算譜意味論(プログラムの数理モデル)、算譜検証論(プログラムの正しさの検証、妥当性確認)など、プログラムに関する数理科学的研究を行います。コンピュータのハードウェアやソフトウェアに限らず、それを使う人々を含めた、広い意味での情報処理システムのライフサイクルを取り扱います。研究対象はプログラムやシステムの仕様書などの記述文書で、例えば、システムの安全・安心に関する議論を記したアシュランスケースとよばれる文書の構造や整合性検査の研究を行っています。組織の規則や標準・規格、法律などへの応用も考えられます。膨大な記述のなかのほんの小さな間違いが、飛行機墜落やプラント事故などの重大な結果を招く場合が多々あります。どのように記述し、整合性を保つのかが研究のテーマです。

研究室紹介

◎教育の方針
○情報システムのお医者さんを育てます。
システムライフサイクルに関する研究です。成果実証の場として、ソフトウェア工学やディペンダビリティ(信頼性)に関する国際標準活動(ISO/IEC SC7, IEC TC56, OMG)にも携わっています。
• システムの診察
システムの不具合の原因究明法を研究します。
• システムの健康診断
不具合がないかどうか調べる方法を研究します。
• システムの健康法
システムの開発、運用、手入れ(保守)の方法を研究します。
• システムのリスク管理法
システムのリスクに関して関係者間で意思疎通を図って合意に至るための手法を研究します。
• システムの診断書発行
システムの信頼性や安全性の基準を研究します。
◎学生指導の進め方
• 初めは教科書購読・論文購読を行います。
この分野の基本的な語彙と考え方を身に付けていただきます。
• できるだけ早い機会に「プロジェクト」に移ります。産業や学界の実地の問題の解決に取り組みます。小さくて簡単かもしれないけれど、創造性を発揮できるテーマを提示するよう努力します。
◎研究環境
• 科学技術研究機構CREST制度によるプロジェクト「利用者指向ディペンダビリティの研究」および国立情報学研究所共同研究「議論の枠組みに関する基礎理論および応用の研究」を遂行しており、第一線の研究者が集まって研究活動に携わっています。
• 国際的な研究交流があります。意味論研究について、英国バース大学と研究交流を続けており、Agdaシステム研究開発については、スウェーデンのシャルマース工科大学と密接な研究交流があります。
Agdaは、プログラミング言語と形式仕様記述言語の二つの側面をうまく併せ持つため、形式手法のツールとして研究に用いています。
• 国内での研究交流も豊富です。教授は産業技術総合研究所でも活動しており、奈良先端科学技術大学院大学の連携講座も担当しています。

 
 
ページの先頭へ