研究課題
基盤研究(C)
グリッドコンピューティング環境上へ実装した定理証明器と，様々なターゲット実装コードを出力可能なハードウェアコンパイラを融合し，上流から下流工程まで一貫した高機能な形式検証系を構築し，非同期並列回路システムの検証能力の飛躍的向上を図る．対象回路の構成情報は，関数型言語系の上で記述し，この言語系からのコンパイラ出力として，ターゲット実装コードと，プルーフチェッカへの証明式の列を同時に得る．対象回路は，非同期論理ゲート素子のモデルを二線式 4 値論理に基づいたメッセージパッシング型並列計算でモデル化し，回路接続の正当性証明はプルーフチェッカーを用いて検証する．
すべて 2013 2012 2011 その他
すべて 雑誌論文 (12件) (うち査読あり 12件) 学会発表 (29件) 備考 (4件)
International Journal of Advanced Computer Science
巻: 3(1) ページ: 26-32
Proceedings of the 2013 International Conference on e-Learning, e-Business, Enterprise Information Systems, and e-Government (EEE'13)
巻: 1 ページ: 321-326
International Journal of Advancements in Computing Technology
巻: 4(14) ページ: 372-380
Formalized Mathematics
巻: 20(1) ページ: 61-63
120007101103
Proceedings of the 9th International Conference on Information Technology : New Generations (ITNG2012)
ページ: 827-830
120007101105
Advances in Information Technology and Applied Computing
巻: 1 ページ: 195-200
DPSWS2012
ページ: 219-226
120007101104
Proceedings of International Conference of Information Science and Computer Applications (ICISCA 2012)
情報処理学会 第20回マルチメディア通信と分散処理ワークショップ (DPSWS2012) 論文集
巻: 1 ページ: 219-226
巻: Vol.3, No.8 ページ: 189-197
Proceedings of the 7th International Conference on Digital Content, Multimedia Technology and its Applications (IDCTA2011)
ページ: 139-144
120007101107
The 8th International Conference on Information Technology : New Generations (ITNG2011)
巻: 1 ページ: 1-6
10.1109/itng.2011.8
120007101106
http://soar-rd.shinshu-u.ac.jp/profile/ja.gCnejaTN.html#books_articles_etc
http://markun.cs.shinshu-u.ac.jp/mirror/mizar/
http://versita.metapress.com/content/121073/
http://hips-tools.sourceforge.net/wiki/
