| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2011-11-14 15:35 Mizarによる数論アルゴリズムの形式化と検証 ○青木祥希・岡崎裕之・師玉康成（信州大）  ISEC2011-44 LOIS2011-38 |
|
| 抄録 | （和） | 本稿では数論アルゴリズムからユークリッドの互除法と拡張ユークリッドの互除法を取り上げ， プルーフチェッカ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 / / / / / | |
| 文献情報 | 信学技報, vol. 111, no. 285, ISEC2011-44, pp. 69-74, 2011年11月. | |
| 資料番号 | ISEC2011-44 | |
| 発行日 | 2011-11-07 (ISEC, LOIS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | ISEC2011-44 LOIS2011-38 |
|
| 研究会情報 | |
| 研究会 | ISEC LOIS |
| 開催期間 | 2011-11-14 - 2011-11-15 |
| 開催地（和） | 大阪電気通信大学 |
| 開催地（英） | Osaka Electro-Communication University |
| テーマ（和） | 情報セキュリティ，ライフログ活用技術，ライフインテリジェンス，オフィス情報システム，一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | ISEC |
| 会議コード | 2011-11-ISEC-LOIS |
| 本文の言語 | 日本語 |
| タイトル（和） | Mizarによる数論アルゴリズムの形式化と検証 |
| サブタイトル（和） | |
| タイトル（英） | Formalization and Verification of Arithmetic Algorithms by Mizar |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 形式的検証 / formal verification |
| キーワード(2)（和/英） | Mizar / Mizar |
| キーワード(3)（和/英） | 拡張ユークリッドの互除法 / Extended Euclidean Algorithm |
| キーワード(4)（和/英） | / |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 青木 祥希 / Yoshiki Aoki / アオキ ヨシキ |
| 第1著者 所属（和/英） | 信州大学 (略称： 信州大) Shinshu University (略称： Shinshu Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 岡崎 裕之 / Hiroyuki Okazaki / オカザキ ヒロユキ |
| 第2著者 所属（和/英） | 信州大学 (略称： 信州大) Shinshu University (略称： Shinshu Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 師玉 康成 / Yasunari Shidama / シダマ ヤスナリ |
| 第3著者 所属（和/英） | 信州大学 (略称： 信州大) Shinshu University (略称： Shinshu Univ.) |
| 第4著者 氏名（和/英/ヨミ） | / / |
| 第4著者 所属（和/英） | (略称： ) (略称： ) |
| 第5著者 氏名（和/英/ヨミ） | / / |
| 第5著者 所属（和/英） | (略称： ) (略称： ) |
| 第6著者 氏名（和/英/ヨミ） | / / |
| 第6著者 所属（和/英） | (略称： ) (略称： ) |
| 第7著者 氏名（和/英/ヨミ） | / / |
| 第7著者 所属（和/英） | (略称： ) (略称： ) |
| 第8著者 氏名（和/英/ヨミ） | / / |
| 第8著者 所属（和/英） | (略称： ) (略称： ) |
| 第9著者 氏名（和/英/ヨミ） | / / |
| 第9著者 所属（和/英） | (略称： ) (略称： ) |
| 第10著者 氏名（和/英/ヨミ） | / / |
| 第10著者 所属（和/英） | (略称： ) (略称： ) |
| 第11著者 氏名（和/英/ヨミ） | / / |
| 第11著者 所属（和/英） | (略称： ) (略称： ) |
| 第12著者 氏名（和/英/ヨミ） | / / |
| 第12著者 所属（和/英） | (略称： ) (略称： ) |
| 第13著者 氏名（和/英/ヨミ） | / / |
| 第13著者 所属（和/英） | (略称： ) (略称： ) |
| 第14著者 氏名（和/英/ヨミ） | / / |
| 第14著者 所属（和/英） | (略称： ) (略称： ) |
| 第15著者 氏名（和/英/ヨミ） | / / |
| 第15著者 所属（和/英） | (略称： ) (略称： ) |
| 第16著者 氏名（和/英/ヨミ） | / / |
| 第16著者 所属（和/英） | (略称： ) (略称： ) |
| 第17著者 氏名（和/英/ヨミ） | / / |
| 第17著者 所属（和/英） | (略称： ) (略称： ) |
| 第18著者 氏名（和/英/ヨミ） | / / |
| 第18著者 所属（和/英） | (略称： ) (略称： ) |
| 講演者 | 1 |
| 発表日時 | 2011-11-14 15:35:00 |
| 発表時間 | 25 |
| 申込先研究会 | ISEC |
| 資料番号 | IEICE-ISEC2011-44,IEICE-LOIS2011-38 |
| 巻番号（vol） | IEICE-111 |
| 号番号（no） | no.285(ISEC), no.286(LOIS) |
| ページ範囲 | pp.69-74 |
| ページ数 | IEICE-6 |
| 発行日 | IEICE-ISEC-2011-11-07,IEICE-LOIS-2011-11-07 |
[研究会発表申込システムのトップページに戻る]