Programming Logic Laboratory
プログラム論理研究室

[Japanese/English]

研究内容

｢ソフトウェアの正しさの保証」が大目標です。そのために、論理に基づくソフトウェアの基礎理論を構築し、それをソフトウェアの検証、合成、変換等に応用する研究を行っています。

• プログラムの論理：ラムダ計算と型理論に基づくプログラム言語の理論と応用
  
  多くの先進的なプログラム言語の中核には、関数の概念と型システムがあります。これらの性質を研究することにより、プログラミングの本質が見えてきます。これを通して、プログラム（計算）の意味を明確にし、プログラムの検証、合成、（正しい）変換　等をおこないます。
  
  • 研究テーマの例：　コントロール機構（continuation)の計算系、環境や文脈を扱う 計算系、型システムと論理
  　
  プログラム変換は、正しさを保ちつつ、効率的なプログラムへ変換する技法です。 　ここでは、部分計算の手法により、変換技法について研究します。 　部分計算とは、「ｘのy乗」を計算するときに、ｙの値が３であるとわかっていたら、 再起呼び出し（もしくは繰り返し文)を全部展開した、効率よいプログラム（x*x*x）を得られる、という 洞察に基づく技法です。
  
  • 研究テーマの例：　定理証明システムの部分計算、 部分計算の定式化、部分計算を行うシステムの構築
  　
  さらに、これらの研究を従来型の計算モデル（閉じた環境の中だけで計算を進めるモデル）だけではなく、オープン計算モデル（他のコンピュータ等とのコミュニケーションにより計算が進むというモデル）に適用するための研究をおこなっています。

• モデル検査や定理証明によるソフトウェアの検証
  
  ソフトウェアの検証とは、ソフトウェアが「正しい」ことを証明することです。ソフトウェア検証への有力なアプローチである定理証明とモデル検査について研究をしています。
  定理証明は、ソフトウェアの正当性を論理式として表現し、数学的な定理証明を行うソフトウェアを用いてコンピュータ上で検証する手法です。 　　
  モデル検査は、有限状態のシステム(ソフトウェア、ハードウェア、そのほか）がある種の性質を満たすことを網羅的な探索により示す手法であり、近年の 計算パワーの上昇により非常に広い範囲のシステムの検証に用いられている 極めてホットな話題です。非常に状態数の多いシステムへの対処、 無限状態システムへの対処、実時間の記述、等々の拡張が待たれています。
  
  • 研究テーマの例：　モデル検査による並列アルゴリズムの検証、 実時間モデル検査の研究、モデル検査システムや定理証明システムのユーザインターフェースの作成
    

プログラム論理研究室ホームページ