2002 Fiscal Year Annual Research Report

書換え技術に基づくソフトウエア解析

Research Project

Project/Area Number	14019007
Research Institution	University of Tsukuba
Principal Investigator	MIDDELDORP Aart 筑波大学, 電子・情報工学系, 助教授 (30251044)
Keywords	項書換え系 / 記号計算 / 停止性 / 自動化
Research Abstract	停止性を保証する問題は計算機科学の多くの分野で生じる。様々なプログラミング言語においてプログラムが停止することを証明するために、多くの研究がなされてきた。ソフトウェア解析のテクニックであるプログラムの特殊化,部分評価,プログラム変換は、いずれも基盤技術として停止性が必須である。またセーフティクリティカルなシステムでは、正しい動作を保証する必要があるが、このような問題の多くは項書換え系の停止性問題へと帰着させることが可能である。項書換え系の停止性証明の自動化は、従来、単純化順序をベースにしたテクニックを用いていたが、この数年間においては、単純化順序の持つ限界を打破する自動化手法の研究が盛んに行われるようになった。ArtsとGieslの依存対法は、現在注目されている新手法の1つである。依存対法に基づく停止性証明ツールの実現する際には、(1)依存グラフの近似,(2)循環解析,(3)引数フィルタリングの3つの困難がある。最初の2つにより、停止性を証明するために解かなければならない順序制約の集合(連立不等式の一種)の数とサイズが決まる。3つ目により、順序制約の集合を解く際の探索空間のサイズが決まる。これらのサイズと停止性証明の計算コストは比例するが、私たちは新たなアルゴリズムを開発し、そのサイズを劇的に削減することに成功した。このアルゴリズムを停止性自動証明ツールTsukuba Termination Tool上で実装し、数多くの実験を行った。その実験データによりアルゴリズムの有効性が確認された。

Research Products
(4 results)

All Other

All Publications (4 results)

[Publications] Aart Middeldorp: "Approximations for Strategies and Termination"Proceedings of the 2nd International Workshop on Reduction Strategies in Rewriting and Programming, Electronic Notes in Computer Science. 70(6). (2002)
[Publications] Jurgen Giesl, Aart Middeldorp: "Innermost Termination of Context-Sensitive Rewriting"Proceedings of the 6th International Conference on Developments in Language Theory, Lecture Notes in Computer Science. (印刷中). (2003)
[Publications] Alfons Geser, Aart Middeldorp, Enno Ohlebusch, Hans Zantema: "Relative Undecidability in Term Rewriting, Part 1 : The Termination Hierarchy"Information and Computation. 178(1). 101-131 (2002)
[Publications] Alfons Geser, Aart Middeldorp, Enno Ohlebusch, Hans Zantema: "Relative Undecidability in Term Rewriting, Part 2 : The Confluence Hierarchy"Information and Computation. 178(1). 132-148 (2002)

2002 Fiscal Year Annual Research Report

書換え技術に基づくソフトウエア解析

Principal Investigator

MIDDELDORP Aart 筑波大学, 電子・情報工学系, 助教授 (30251044)

Research Products

[Publications] Aart Middeldorp: "Approximations for Strategies and Termination"Proceedings of the 2nd International Workshop on Reduction Strategies in Rewriting and Programming, Electronic Notes in Computer Science. 70(6). (2002)

[Publications] Jurgen Giesl, Aart Middeldorp: "Innermost Termination of Context-Sensitive Rewriting"Proceedings of the 6th International Conference on Developments in Language Theory, Lecture Notes in Computer Science. (印刷中). (2003)

[Publications] Alfons Geser, Aart Middeldorp, Enno Ohlebusch, Hans Zantema: "Relative Undecidability in Term Rewriting, Part 1 : The Termination Hierarchy"Information and Computation. 178(1). 101-131 (2002)

[Publications] Alfons Geser, Aart Middeldorp, Enno Ohlebusch, Hans Zantema: "Relative Undecidability in Term Rewriting, Part 2 : The Confluence Hierarchy"Information and Computation. 178(1). 132-148 (2002)