| 講演名 | 2023-10-11 相互排除アルゴリズムを対象とした形式検証技術の適用 西口 尚輝(阪大), 土屋 達弘(阪大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 並行アルゴリズムを正しく設計するのは難しい．本研究では，相互排除に注目し，並行アルゴリズムを仕様化し検証する形式手法の利点をケーススタディを通じて探る．ケーススタディから得られた知見を，検証したアルゴリズムの1つで検出されたエラーとともに報告する． |
| 抄録(英) | |
| キーワード(和) | モデル検査 / 相互排除 / TLA+ / PlusCal / 形式仕様記述 |
| キーワード(英) | |
| 資料番号 | SS2023-24,DC2023-30 |
| 発行日 | 2023-10-04 (SS, DC) |
| 研究会情報 | |
| 研究会 | SS / DC |
|---|---|
| 開催期間 | 2023/10/11(から2日開催) |
| 開催地（和） | 信州大学工学部（長野市） |
| 開催地（英） | |
| テーマ（和） | ディペンダブルコンピューティング，ソフトウェアサイエンスおよび一般 |
| テーマ（英） | |
| 委員長氏名（和） | 岡野 浩三(信州大) / 土屋 達弘(阪大) |
| 委員長氏名（英） | Kozo Okano(Shinshu Univ.) / Tatsuhiro Tsuchiya(Osaka Univ.) |
| 副委員長氏名（和） | 肥後 芳樹(阪大) / 細川 利典(日大) |
| 副委員長氏名（英） | Yoshiki Higo(Osaka Univ.) / Toshinori Hosokawa(Nihon Univ.) |
| 幹事氏名（和） | 小形 真平(信州大) / 林 晋平(東工大) / 新井 雅之(日大) / 難波 一輝(千葉大) |
| 幹事氏名（英） | Shinpei Ogata(Shinshu Univ.) / Shinpei Hayashi(Tokyo Inst. of Tech.) / Masayuki Arai(Nihon Univ.) / Kazuteru Namba(Chiba Univ.) |
| 幹事補佐氏名（和） | ?本 真佑(阪大) |
| 幹事補佐氏名（英） | Shinsuke Matsumoto(Osaka Univ.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Software Science / Technical Committee on Dependable Computing |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 相互排除アルゴリズムを対象とした形式検証技術の適用 |
| サブタイトル（和） | |
| タイトル（英） | Formal Verification of Concurrent Algorithms: Case Studies on Mutual Exclusion |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデル検査 |
| キーワード(2)（和/英） | 相互排除 |
| キーワード(3)（和/英） | TLA+ |
| キーワード(4)（和/英） | PlusCal |
| キーワード(5)（和/英） | 形式仕様記述 |
| 第 1 著者 氏名（和/英） | 西口 尚輝 / Naoki Nishiguchi |
| 第 1 著者 所属（和/英） | 大阪大学(略称：阪大) Osaka University(略称：Osaka Univ.) |
| 第 2 著者 氏名（和/英） | 土屋 達弘 / Tatsuhiro Tsuchiya |
| 第 2 著者 所属（和/英） | 大阪大学(略称：阪大) Osaka University(略称：Osaka Univ.) |
| 発表年月日 | 2023-10-11 |
| 資料番号 | SS2023-24,DC2023-30 |
| 巻番号（vol） | vol.123 |
| 号番号（no） | SS-206,DC-207 |
| ページ範囲 | pp.19-21(SS), pp.19-21(DC), |
| ページ数 | 3 |
| 発行日 | 2023-10-04 (SS, DC) |