| Presentation | 2019-01-16 On Representation of Structures and Unions in Logically Constrained Rewriting Yoshiaki Kanazawa, Naoki Nishida, Masahiko Sakai, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Recently, several methods for verifying imperative programs by means of transformations into term rewriting systems have been investigated. In particular, constrained rewriting systems are popular as sources of such transformations, since logical constraints used for modeling control flows can be separated from terms that represent intermediate states of the execution of target programs.In the existing methods, data types that can be used in target programs are, however, restricted to the integers and their one-dimensional arrays, and hence we are not allowed to use other primitive data types, structures, or unions.In this article, we propose a bit-vector representation of basic data types that are recursively defined over size-fixed primitive data types, structure, and unions in the framework of logically constrained rewriting, and then propose a construction of rewrite rules that access members of structures and unions. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | logically constrained rewriting / program transformation / bit vector / structure / union |
| Paper # | MSS2018-67,SS2018-38 |
| Date of Issue | 2019-01-08 (MSS, SS) |
| Conference Information | |
| Committee | MSS / SS |
|---|---|
| Conference Date | 2019/1/15(2days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | Morikazu Nakamura(Univ. of Ryukyus) / Akio Nakata(Hiroshima City Univ.) |
| Vice Chair | Shigemasa Takai(Osaka Univ.) / Takashi Kobayashi(Tokyo Inst. of Tech.) |
| Secretary | Shigemasa Takai(Toshiba) / Takashi Kobayashi(Osaka Univ.) |
| Assistant | Hideki Kinjo(Okinawa Univ.) / Shinpei Hayashi(Tokyo Inst. of Tech.) |
| Paper Information | |
| Registration To | Technical Committee on Mathematical Systems Science and its applications / Technical Committee on Software Science |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | On Representation of Structures and Unions in Logically Constrained Rewriting |
| Sub Title (in English) | |
| Keyword(1) | logically constrained rewriting |
| Keyword(2) | program transformation |
| Keyword(3) | bit vector |
| Keyword(4) | structure |
| Keyword(5) | union |
| 1st Author's Name | Yoshiaki Kanazawa |
| 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.) |
| Date | 2019-01-16 |
| Paper # | MSS2018-67,SS2018-38 |
| Volume (vol) | vol.118 |
| Number (no) | MSS-384,SS-385 |
| Page | pp.pp.67-72(MSS), pp.67-72(SS), |
| #Pages | 6 |
| Date of Issue | 2019-01-08 (MSS, SS) |