| Presentation | 2006-10-26 Approach to Software Verification Based on Transformation from Procedural Programs to Rewrite Systems Yuki FURUICHI, Naoki NISHIDA, Masahiko SAKAI, Keiichiro KUSAKARI, Toshiki SAKABE, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(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) |
| Keyword(in English) | term rewriting system / inductive theorem / inductionless induction / Presburuger arithmetic / completion / program transformation |
| Paper # | SS2006-41,KBSE2006-17 |
| Date of Issue |
| Conference Information | |
| Committee | SS |
|---|---|
| Conference Date | 2006/10/19(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Software Science (SS) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Approach to Software Verification Based on Transformation 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) | Presburuger arithmetic |
| Keyword(5) | completion |
| Keyword(6) | program transformation |
| 1st Author's Name | Yuki FURUICHI |
| 1st Author's Affiliation | Graduate School of Information Science, Nagoya University() |
| 2nd Author's Name | Naoki NISHIDA |
| 2nd Author's Affiliation | Graduate School of Information Science, Nagoya University |
| 3rd Author's Name | Masahiko SAKAI |
| 3rd Author's Affiliation | Graduate School of Information Science, Nagoya University |
| 4th Author's Name | Keiichiro KUSAKARI |
| 4th Author's Affiliation | Graduate School of Information Science, Nagoya University |
| 5th Author's Name | Toshiki SAKABE |
| 5th Author's Affiliation | Graduate School of Information Science, Nagoya University |
| Date | 2006-10-26 |
| Paper # | SS2006-41,KBSE2006-17 |
| Volume (vol) | vol.106 |
| Number (no) | 324 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |