| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2023-03-15 09:30 ビットベクトル制約付き項書換え系の停止性証明のための多項式解釈プロセッサについて ○松見歩佳・西田直樹・小嶋美咲・申 東訓（名大）  SS2022-61 |
|
| 抄録 | （和） | ビットベクトル制約付き項書換え系（BV-LCTRS）はC言語などのプログラムのモデルとして有用である．等価性検証に書換え帰納法を用いる際には，与えられた書換え系に帰納法の仮定となる書換え規則を加えて得られる書換え系の停止性が何度も証明される. LCTRSの停止性証明には項書換え系と同様に依存対プロセッサを使用して証明する枠組みの依存対フレームワークが用いられるが，整数制約を持つLCTRSの停止性証明において最も強力なプロセッサの1つである多項式解釈プロセッサはBV-LCTRSには適用できない．本稿では，BV-LCTRSの停止性証明を強化することを目的として，新たな依存対プロセッサとしてビットベクトル上の多項式解釈プロセッサと単一自己ループ除去プロセッサを提案する． |
| （英） | 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. | |
| キーワード | （和） | プログラム検証 / 制約付き書換え / 依存対フレームワーク / ビットベクトル算術 / / / / |
| （英） | program verification / constrained rewriting / dependency pair framework / bit-vector arithmetic / / / / | |
| 文献情報 | 信学技報, vol. 122, no. 432, SS2022-61, pp. 85-90, 2023年3月. | |
| 資料番号 | SS2022-61 | |
| 発行日 | 2023-03-07 (SS) | |
| ISSN | Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2022-61 |
|
| 研究会情報 | |
| 研究会 | SS |
| 開催期間 | 2023-03-14 - 2023-03-15 |
| 開催地（和） | 名護市産業支援センター |
| 開催地（英） | |
| テーマ（和） | ソフトウェアサイエンスおよび一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2023-03-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | ビットベクトル制約付き項書換え系の停止性証明のための多項式解釈プロセッサについて |
| サブタイトル（和） | |
| タイトル（英） | On Polynomial Interpretations Toward Termination of Logically Constrained Term Rewrite Systems with Bit Vector Arithmetic |
| サブタイトル（英） | |
| キーワード(1)（和/英） | プログラム検証 / program verification |
| キーワード(2)（和/英） | 制約付き書換え / constrained rewriting |
| キーワード(3)（和/英） | 依存対フレームワーク / dependency pair framework |
| キーワード(4)（和/英） | ビットベクトル算術 / bit-vector arithmetic |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 松見 歩佳 / Ayuka Matsumi / マツミ アユカ |
| 第1著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 西田 直樹 / Naoki Nishida / ニシダ ナオキ |
| 第2著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 小嶋 美咲 / Misaki Kojima / コジマ ミサキ |
| 第3著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第4著者 氏名（和/英/ヨミ） | 申 東訓 / Donghoon Shin / シン ドンフン |
| 第4著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第5著者 氏名（和/英/ヨミ） | / / |
| 第5著者 所属（和/英） | (略称： ) (略称： ) |
| 第6著者 氏名（和/英/ヨミ） | / / |
| 第6著者 所属（和/英） | (略称： ) (略称： ) |
| 講演者 | 第1著者 |
| 発表日時 | 2023-03-15 09:30:00 |
| 発表時間 | 25分 |
| 申込先研究会 | SS |
| 資料番号 | SS2022-61 |
| 巻番号（vol） | vol.122 |
| 号番号（no） | no.432 |
| ページ範囲 | pp.85-90 |
| ページ数 | 6 |
| 発行日 | 2023-03-07 (SS) |
[研究会発表申込システムのトップページに戻る]