講演抄録/キーワード |
講演名 |
2011-03-08 09:25
プログラム変換を用いたポインタ操作プログラムの検証にむけて ~ Morrisの二分木走査アルゴリズムによるケーススタディ ~ ○渡部卓雄・森口草介・山田一宏・西崎真也(東工大) SS2010-69 |
抄録 |
(和) |
ポインタ書き換えを伴うプログラムのプログラム変換にもとづく検証のケーススタディとして,
Morrisの二分木走査アルゴリズムの正当性を扱った.
本稿ではその際に用いたプログラム変換手法とその具体的な適用手法について報告する. |
(英) |
We proved the correctness of a C implementation of Morris's tree traversal algorithm.
The algorithm is known as a recursion-free, stack-free and tag-free binary tree traversal.
This work is intended to be a case study of verifying C programs with pointer manipulation
by using program transformation.
In this report, we describe the outline of the verification methodology and results. |
キーワード |
(和) |
プログラム検証 / プログラム変換 / ポインタ操作 / Morrisの二分木走査アルゴリズム / / / / |
(英) |
program verification / program transformation / pointer manipulation / Morris' tree traversal algorithm / / / / |
文献情報 |
信学技報, vol. 110, no. 458, SS2010-69, pp. 97-102, 2011年3月. |
資料番号 |
SS2010-69 |
発行日 |
2011-02-28 (SS) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
SS2010-69 |