| 研究課題/領域番号 |
16K00091
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| 研究分担者 |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2019-03-31
|
| 研究課題ステータス |
完了 (2018年度)
|
| 配分額 *注記 |
3,510千円 (直接経費: 2,700千円、間接経費: 810千円)
2018年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2017年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2016年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
|
|---|
| キーワード | 書き換えシステム / プログラム検証 |
|---|
| 研究成果の概要 |
書き換えシステムに基づく新しいプログラム検証手法を開発することを目的として研究を進めた。研究成果の概要は以下の通りである。
(1) 束縛変数を伴う書き換えシステムに対して、名目書き換えシステムと関連する体系における合流性の判定条件についての成果が得られた。また、高階の書き換え体系に対する合流性・停止性の自動判定システムの開発に参加し、国際競技会において良い成績を収めた。
(2) 文脈移動変換と関連する帰納的定理証明の手法に対して、十分完全性を持たない書き換えシステムにおける潜在帰納法についての考察から、無限リストのような計算が停止しない式を含むプログラムに適用可能な新しい検証手法を開発した。
|
| 研究成果の学術的意義や社会的意義 |
束縛変数を伴う書き換えシステムに対する合流性や停止性についての研究及びその成果は、従来の第一階項書き換えシステムに基づく帰納的定理証明手法である潜在帰納法および書き換え帰納法を、高階項に対する書き換えシステムに基づく手法へ拡張するにあたって重要になると考えられる。また、十分完全性を持たない書き換えシステムにおける潜在帰納法についての研究及びその成果は、入力によって計算が停止しない様々なプログラムに対する検証手法を開発するにあたって重要になると考えられる。これらの成果を利用したプログラム及びプログラミング言語に対する検証手法は、ソフトウェアの信頼性を向上させる技術として役立つことが期待できる。
|
