以前チェックした研究室

画面を閉じる
画面を閉じる
理学部
情報科学科
戻る
  • 数学系
  • 情報学系

木下 佳樹 研究室

プログラミングの原理を科学する

研究キーワード
  • プログラム意味論
  • 検証
  • 妥当性確認
  • 数理的手法
木下 佳樹 研究室
コンピュータプログラムとオープンシステムディペンダビリティに関する書籍

当研究室のテーマである「プログラミング科学」とは、プログラムとは何か?(算譜意味論)、正しいプログラムとは?(算譜検証論)、システムが妥当とは?(妥当性確認論) という三つの問いから出発する、プログラム構築に関する科学です。
算譜意味論には圏論、普遍代数などを用います。算譜検証論には、命題論理や述語論理だけでなく、時相論理や構成的型理論などの特別な体系を用います。妥当性確認論では、アシュランスケースと呼ばれる形式を用います。
当研究室では、算譜意味論や算譜検証論の手法を応用した形式アシュランスケース、システム利用者を含めた情報処理システムライフサイクルなどを数理科学の立場から研究しています。

木下 佳樹教授Kinoshita Yoshiki[理学部/情報科学科]

専門分野
  • ソフトウェア科学
  • プログラム意味論
主な担当科目
関連リンク
PROFESSOR's VOICEPROFESSOR's VOICE

意図通りに動くプログラム構築を研究

木下 佳樹教授

プログラム「で」研究するのではなく、プログラム「を」研究します。プログラムが意図通りに動くことを確信できるようにするために、プログラムや関連文書を解析する方法を、数理科学の立場から研究します。

この研究室もチェック!