| Presentation | 2023-03-15 On Polynomial Interpretations Toward Termination of Logically Constrained Term Rewrite Systems with Bit Vector Arithmetic Ayuka Matsumi, Naoki Nishida, Misaki Kojima, Donghoon Shin, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Logically constrained term rewrite systems with the bit-vector theory (BV-LCTRSs, for short) are useful as models of programs written in C or other languages. During a process of Rewriting Induction for equivalence verification, we need to frequently prove termination of rewrite systems obtained by adding rewriting rules for induction hypotheses into a given rewrite system. As for term rewrite systems, the dependency pair (DP, for short) framework is used for proving termination of LCTRSs, and several kinds of DP processors are used in the framework. However, the polynomial interpretation processor, one of the most powerful processors in proving termination of LCTRSs with the integer theory, is not applicable to BV-LCTRSs. In this article, we aim at enhancing the power of proving termination of BV-LCTRSs. To this end, we propose the polynomial interpretation processor over bit-vectors and the single self-looping elimination processor as new DP processors for BV-LCTRSs. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | program verification / constrained rewriting / dependency pair framework / bit-vector arithmetic |
| Paper # | SS2022-61 |
| Date of Issue | 2023-03-07 (SS) |
| Conference Information | |
| Committee | SS |
|---|---|
| Conference Date | 2023/3/14(2days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | Kozo Okano(Shinshu Univ.) |
| Vice Chair | Yoshiki Higo(Osaka Univ.) |
| Secretary | Yoshiki Higo(Shinshu Univ.) |
| Assistant | Shinsuke Matsumoto(Osaka Univ.) |
| Paper Information | |
| Registration To | Technical Committee on Software Science |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | On Polynomial Interpretations Toward Termination of Logically Constrained Term Rewrite Systems with Bit Vector Arithmetic |
| Sub Title (in English) | |
| Keyword(1) | program verification |
| Keyword(2) | constrained rewriting |
| Keyword(3) | dependency pair framework |
| Keyword(4) | bit-vector arithmetic |
| 1st Author's Name | Ayuka Matsumi |
| 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 | Misaki Kojima |
| 3rd Author's Affiliation | Nagoya University(Nagoya Univ.) |
| 4th Author's Name | Donghoon Shin |
| 4th Author's Affiliation | Nagoya University(Nagoya Univ.) |
| Date | 2023-03-15 |
| Paper # | SS2022-61 |
| Volume (vol) | vol.122 |
| Number (no) | SS-432 |
| Page | pp.pp.85-90(SS), |
| #Pages | 6 |
| Date of Issue | 2023-03-07 (SS) |