| 講演名 | 2011-11-14 Mizarによる数論アルゴリズムの形式化と検証(一般,情報セキュリティ,ライフログ活用技術,ライフインテリジェンス,オフィス情報システム,一般) 青木 祥希, 岡崎 裕之, 師玉 康成, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本稿では数論アルゴリズムからユークリッドの互除法と拡張ユークリッドの互除法を取り上げ,プルーフチェッカMizarを用いて形式化を行う.本研究での目的は数論を扱うツールの実装を支援することである.本研究で形式化を行ったアルゴリズムは数論システムであるNZMATHのソースコードに基づいている. |
| 抄録(英) | In this report, we formalize some number theoretical algorithms, Euclidean Algorithm and Extended Euclidean Algorithm by using the Mizar proof checker. Our aim is to support implementation of number theoretic tools. Our formalization of those algorithms are based on the source code of the NZMATH, a number theory oriented calculation system. |
| キーワード(和) | 形式的検証 / Mizar / 拡張ユークリッドの互除法 |
| キーワード(英) | formal verification / Mizar / Extended Euclidean Algorithm |
| 資料番号 | ISEC2011-44,LOIS2011-38 |
| 発行日 |
| 研究会情報 | |
| 研究会 | ISEC |
|---|---|
| 開催期間 | 2011/11/7(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Information Security (ISEC) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | Mizarによる数論アルゴリズムの形式化と検証(一般,情報セキュリティ,ライフログ活用技術,ライフインテリジェンス,オフィス情報システム,一般) |
| サブタイトル（和） | |
| タイトル（英） | Formalization and Verification of Arithmetic Algorithms by Mizar |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 形式的検証 / formal verification |
| キーワード(2)（和/英） | Mizar / Mizar |
| キーワード(3)（和/英） | 拡張ユークリッドの互除法 / Extended Euclidean Algorithm |
| 第 1 著者 氏名（和/英） | 青木 祥希 / Yoshiki AOKI |
| 第 1 著者 所属（和/英） | 信州大学 Shinshu University |
| 第 2 著者 氏名（和/英） | 岡崎 裕之 / Hiroyuki OKAZAKI |
| 第 2 著者 所属（和/英） | 信州大学 Shinshu University |
| 第 3 著者 氏名（和/英） | 師玉 康成 / Yasunari SHIDAMA |
| 第 3 著者 所属（和/英） | 信州大学 Shinshu University |
| 発表年月日 | 2011-11-14 |
| 資料番号 | ISEC2011-44,LOIS2011-38 |
| 巻番号（vol） | vol.111 |
| 号番号（no） | 285 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |