電子情報通信学会 研究会発表申込システム
講演論文 詳細
技報閲覧サービス
技報オンライン
‥‥ (ESS/通ソ/エレソ/ISS)
技報アーカイブ
‥‥ (エレソ)
 トップに戻る 前のページに戻る   [Japanese] / [English] 

講演抄録/キーワード
講演名 2011-11-14 15:35
Mizarによる数論アルゴリズムの形式化と検証
青木祥希岡崎裕之師玉康成信州大
技報オンラインサービス実施中
抄録 (和) 本稿では数論アルゴリズムからユークリッドの互除法と拡張ユークリッドの互除法を取り上げ,
プルーフチェッカ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

研究会情報
研究会 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著者 所属(和/英) (略称: )
(略称: )
講演者
発表日時 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 


[研究会発表申込システムのトップページに戻る]

[電子情報通信学会ホームページ]


IEICE / 電子情報通信学会