| IEICE Technical Committee Submission System Conference Paper's Information |
Online Proceedings [Sign in] Tech. Rep. Archives |
| Go Top Page | Go Previous | [Japanese] / [English] |
| Paper Abstract and Keywords | ||
| Presentation | 2023-03-15 09:30 On Polynomial Interpretations Toward Termination of Logically Constrained Term Rewrite Systems with Bit Vector Arithmetic Ayuka Matsumi, Naoki Nishida, Misaki Kojima, Donghoon Shin (Nagoya Univ.)  SS2022-61 |
|
| Abstract | (in Japanese) | (See Japanese page) |
| (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) |
| (in English) | program verification / constrained rewriting / dependency pair framework / bit-vector arithmetic / / / / | |
| Reference Info. | IEICE Tech. Rep., vol. 122, no. 432, SS2022-61, pp. 85-90, March 2023. | |
| Paper # | SS2022-61 | |
| Date of Issue | 2023-03-07 (SS) | |
| ISSN | Online edition: ISSN 2432-6380 | |
| Copyright and reproduction |
All rights are reserved and no part of this publication may be reproduced or transmitted in any form or by any means, electronic or mechanical, including photocopy, recording, or any information storage and retrieval system, without permission in writing from the publisher. Notwithstanding, instructors are permitted to photocopy isolated articles for noncommercial classroom use without fee. (License No.: 10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| Download PDF | SS2022-61 |
|
| Conference Information | |
| Committee | SS |
| Conference Date | 2023-03-14 - 2023-03-15 |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Paper Information | |
| Registration To | SS |
| Conference Code | 2023-03-SS |
| Language | Japanese |
| 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 |
| Keyword(5) | |
| Keyword(6) | |
| Keyword(7) | |
| Keyword(8) | |
| 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.) |
| 5th Author's Name | |
| 5th Author's Affiliation | () |
| 6th Author's Name | |
| 6th Author's Affiliation | () |
| Speaker | Author-1 |
| Date Time | 2023-03-15 09:30:00 |
| Presentation Time | 25 minutes |
| Registration for | SS |
| Paper # | SS2022-61 |
| Volume (vol) | vol.122 |
| Number (no) | no.432 |
| Page | pp.85-90 |
| #Pages | 6 |
| Date of Issue | 2023-03-07 (SS) |
[Return to Top Page]