| Paper Abstract and Keywords |
| Presentation |
2006-10-26 13:40
Approach to Software Verification Based on Transforming from Procedural Programs to Rewrite Systems
Yuki Furuichi, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari, Toshiki Sakabe (Nagoya Univ.) |
| Abstract |
(in Japanese) |
(See Japanese page) |
| (in English) |
In the field of term rewriting, inductionless induction and rewriting
induction have been widely studied as methods for proving inductive
theorems.
Since equivalence of functions (that is, the output values are the
same for the same input) can be represented as an inductive theorem, methods
for proving inductive theorems are useful to verify the equivalence of
functions in functional programming.
In this paper, we try to take advantage of methods for proving
inductive theorems in verifying procedural programs written in
a subset of the C language with integer type.
More precisely, we propose a transformation from procedural programs to
rewrite systems and show that the transformation reduces the equivalence of
procedural programs to that of functions in rewrite systems. |
| Keyword |
(in Japanese) |
(See Japanese page) |
| (in English) |
term rewriting system / inductive theorem / inductionless induction / presburger arithmetic / completion / program transformation / / |
| Reference Info. |
IEICE Tech. Rep., vol. 106, no. 324, SS2006-41, pp. 7-12, Oct. 2006. |
| Paper # |
SS2006-41 |
| Date of Issue |
2006-10-19 (SS, KBSE) |
| ISSN |
Print edition: ISSN 0913-5685 |
| Download PDF |
|
| Conference Information |
| Committee |
SS KBSE |
| Conference Date |
2006-10-26 - 2006-10-27 |
| Place (in Japanese) |
(See Japanese page) |
| Place (in English) |
Ehime University |
| Topics (in Japanese) |
(See Japanese page) |
| Topics (in English) |
|
| Paper Information |
| Registration To |
SS |
| Conference Code |
2006-10-SS-KBSE |
| Language |
Japanese |
| Title (in Japanese) |
(See Japanese page) |
| Sub Title (in Japanese) |
(See Japanese page) |
| Title (in English) |
Approach to Software Verification Based on Transforming from Procedural Programs to Rewrite Systems |
| Sub Title (in English) |
|
| Keyword(1) |
term rewriting system |
| Keyword(2) |
inductive theorem |
| Keyword(3) |
inductionless induction |
| Keyword(4) |
presburger arithmetic |
| Keyword(5) |
completion |
| Keyword(6) |
program transformation |
| Keyword(7) |
|
| Keyword(8) |
|
| 1st Author's Name |
Yuki Furuichi |
| 1st Author's Affiliation |
Nagoya University (Nagoya Univ.) |
| 2nd Author's Name |
Naoki Nishida |
| 2nd Author's Affiliation |
Nagoya University (Nagoya Univ.) |
| 3rd Author's Name |
Masahiko Sakai |
| 3rd Author's Affiliation |
Nagoya University (Nagoya Univ.) |
| 4th Author's Name |
Keiichirou Kusakari |
| 4th Author's Affiliation |
Nagoya University (Nagoya Univ.) |
| 5th Author's Name |
Toshiki Sakabe |
| 5th Author's Affiliation |
Nagoya University (Nagoya Univ.) |
| 6th Author's Name |
|
| 6th Author's Affiliation |
() |
| 7th Author's Name |
|
| 7th Author's Affiliation |
() |
| 8th Author's Name |
|
| 8th Author's Affiliation |
() |
| 9th Author's Name |
|
| 9th Author's Affiliation |
() |
| 10th Author's Name |
|
| 10th Author's Affiliation |
() |
| 11th Author's Name |
|
| 11th Author's Affiliation |
() |
| 12th Author's Name |
|
| 12th Author's Affiliation |
() |
| 13th Author's Name |
|
| 13th Author's Affiliation |
() |
| 14th Author's Name |
|
| 14th Author's Affiliation |
() |
| 15th Author's Name |
|
| 15th Author's Affiliation |
() |
| 16th Author's Name |
|
| 16th Author's Affiliation |
() |
| 17th Author's Name |
|
| 17th Author's Affiliation |
() |
| 18th Author's Name |
|
| 18th Author's Affiliation |
() |
| 19th Author's Name |
|
| 19th Author's Affiliation |
() |
| 20th Author's Name |
|
| 20th Author's Affiliation |
() |
| Speaker |
Author-1 |
| Date Time |
2006-10-26 13:40:00 |
| Presentation Time |
25 minutes |
| Registration for |
SS |
| Paper # |
SS2006-41, KBSE2006-17 |
| Volume (vol) |
vol.106 |
| Number (no) |
no.324(SS), no.326(KBSE) |
| Page |
pp.7-12 |
| #Pages |
6 |
| Date of Issue |
2006-10-19 (SS, KBSE) |
|