A Study on Proof System That Combines Verification and Optimization Technologies

Research Project

Project/Area Number	19500021
Research Category	Grant-in-Aid for Scientific Research (C)
Allocation Type	Single-year Grants
Section	一般
Research Field	Software
Research Institution	Tohoku University
Principal Investigator	OHORI Atsushi Tohoku University, 電気通信研究所, 教授 (60252532)
Project Period (FY)	2007 – 2008
Project Status	Completed (Fiscal Year 2008)
Budget Amount *help	¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000) Fiscal Year 2008: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000) Fiscal Year 2007: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Keywords	プログラミング言語 / コード最適化 / コード検証 / 証明論
Research Abstract	直観主義的論理学の自然演繹証明システムとラムダ計算との同型関係を拡張・一般化し, 機械語コードの証明論を完成し, コードの最適化やコードの検証をより体系的に行う基礎を構築した。この証明論では, 機械語コードは, 左規則のみからなるある種のシーケント計算として表現され, その操作的意味, すなわち, コードを実行する機械の状態遷移規則は, シーケント計算のカット除去定理の証明から系統的に抽出することができる。さらに, この証明システムは, 低レベルコードのアクセス権限の検証や制御フロー遷移の最適化などの基礎となることが示された。

Report

(3 results)