A Study on Proof System That Combines Verification and Optimization Technologies
| 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)
Research Products
(4 results)
