| 講演名 | 2019-01-16 論理制約付き書換えにおける構造体および共用体の表現について 金澤 慶明(名大), 西田 直樹(名大), 酒井 正彦(名大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 近年，項書換え系への変換に基づいた手続き型のプログラムの検証について研究が行われており，実行の中間状態を表現する項から制御フローをモデル化するための論理制約を分離して表現できる論理制約付き項書換え系への変換が注目されている．しかし，既存手法ではデータ型として整数とその1次元配列のみをデータとして扱うC言語プログラムを対象としており，ビット数が異なる基本データ型や構造体，共用体を扱っていない．本稿では，構造体や共用体などのサイズの異なるデータ構造を論理制約付き項書換えの枠組みで扱うための，構造体や共用体のビットベクトルを用いた表現，およびそれらのメンバへアクセスするための書換え規則の構成法を提案する． |
| 抄録(英) | 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. |
| キーワード(和) | 論理制約付き書換え / プログラム変換 / ビットベクトル / 構造体 / 共用体 |
| キーワード(英) | logically constrained rewriting / program transformation / bit vector / structure / union |
| 資料番号 | MSS2018-67,SS2018-38 |
| 発行日 | 2019-01-08 (MSS, SS) |
| 研究会情報 | |
| 研究会 | MSS / SS |
|---|---|
| 開催期間 | 2019/1/15(から2日開催) |
| 開催地（和） | 沖縄県青年会館 |
| 開催地（英） | |
| テーマ（和） | 一般 |
| テーマ（英） | |
| 委員長氏名（和） | 名嘉村 盛和(琉球大) / 中田 明夫(広島市大) |
| 委員長氏名（英） | Morikazu Nakamura(Univ. of Ryukyus) / Akio Nakata(Hiroshima City Univ.) |
| 副委員長氏名（和） | 髙井 重昌(阪大) / 小林 隆志(東工大) |
| 副委員長氏名（英） | Shigemasa Takai(Osaka Univ.) / Takashi Kobayashi(Tokyo Inst. of Tech.) |
| 幹事氏名（和） | 豊嶋 伊知郎(東芝エネルギーシステムズ) / 金澤 尚史(阪大) / 肥後 芳樹(阪大) / 島 和之(広島市大) |
| 幹事氏名（英） | Ichiro Toyoshima(Toshiba) / Takahumi Kanazawa(Osaka Univ.) / Yoshiki Higo(Osaka Univ.) / Kazuyuki Shima(Hiroshima City Univ.) |
| 幹事補佐氏名（和） | 金城 秀樹(沖縄大) / 林 晋平(東工大) |
| 幹事補佐氏名（英） | Hideki Kinjo(Okinawa Univ.) / Shinpei Hayashi(Tokyo Inst. of Tech.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Mathematical Systems Science and its applications / Technical Committee on Software Science |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 論理制約付き書換えにおける構造体および共用体の表現について |
| サブタイトル（和） | |
| タイトル（英） | On Representation of Structures and Unions in Logically Constrained Rewriting |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 論理制約付き書換え / logically constrained rewriting |
| キーワード(2)（和/英） | プログラム変換 / program transformation |
| キーワード(3)（和/英） | ビットベクトル / bit vector |
| キーワード(4)（和/英） | 構造体 / structure |
| キーワード(5)（和/英） | 共用体 / union |
| 第 1 著者 氏名（和/英） | 金澤 慶明 / Yoshiaki Kanazawa |
| 第 1 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 第 2 著者 氏名（和/英） | 西田 直樹 / Naoki Nishida |
| 第 2 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 第 3 著者 氏名（和/英） | 酒井 正彦 / Masahiko Sakai |
| 第 3 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 発表年月日 | 2019-01-16 |
| 資料番号 | MSS2018-67,SS2018-38 |
| 巻番号（vol） | vol.118 |
| 号番号（no） | MSS-384,SS-385 |
| ページ範囲 | pp.67-72(MSS), pp.67-72(SS), |
| ページ数 | 6 |
| 発行日 | 2019-01-08 (MSS, SS) |