| 電子情報通信学会 研究会発表申込システム 研究会 開催スケジュール |
技報閲覧サービス [ログイン] 技報アーカイブ |
すべての研究会開催スケジュール (検索条件: すべての年度)
| 研究会 | 発表日時 | 開催地 | タイトル・著者 | 抄録 | 資料番号 | |
| HWS, VLD (共催) [詳細] |
2020-03-04 10:30 |
沖縄 | 沖縄県青年会館 （開催中止，技報発行あり） |
EVBDDに基づく初等関数回路の設計検証 ○福原浩人・永山 忍・稲木雅人・若林真一（広島市大）  VLD2019-96 HWS2019-69 |
本稿では，EVBDD (Edge-Valued Binary Decision Diagram) に基づく初等関数回路の... [more] | VLD2019-96 HWS2019-69 pp.13-18 |
| VLD | 2016-02-29 13:30 |
沖縄 | 沖縄県青年会館 | Verilog-HDLによる大規模ハードウェア設計の検証支援ツールの開発 ○森光勇太・横川智教（岡山県立大）・近藤真史・宮崎 仁（川崎医療福祉大）・佐藤洋一郎・有本和民（岡山県立大）・吉田則裕（名大） VLD2015-111 |
本稿では，Verilog-HDLで記述された大規模ハードウェア設計の検証支援ツールについて報告する． 検証には，フォー... [more] |
VLD2015-111 pp.1-6 |
| QIT (第二種研究会) |
2015-05-25 13:20 |
大阪 | 大阪大学 | ［ポスター講演］Robertson型不確定性関係の形式的検証 増原孝昭・○栗山十織・吉田雅一・程 俊（同志社大） |
大規模な証明の正当性を検証する方法として，定理証明支援系を用いた形式的検証がある．本研究では，量子鍵配送の無条件安全性に... [more] | |
| MSS | 2015-03-06 10:25 |
石川 | ITビジネスプラザ武蔵 | 割込み遷移削減手法を導入した組込みアセンブリコード向けSMTベースモデル検査器の開発 ○小橋潤平・竹下 淳・山根 智・櫻井孝平（金沢大） MSS2014-100 |
近年の発展を続けている組込みシステムにおいて, ハードウェアに依存する性質を持つソフトウェアが用いられており, 開発期間... [more] | MSS2014-100 pp.53-58 |
| SS | 2014-03-11 11:30 |
沖縄 | てんぷす那覇：第１・２会議室 | JavaにおけるequalsメソッドとhashCodeメソッドの整合性の検査手法の提案 榛葉浩章・○尾ノ上博樹・岡野浩三・楠本真二（阪大） SS2013-75 |
Javaにおいて，コレクションに格納されるオブジェクトはequalsメソッドとhashCodeメソッドをオーバーライドし... [more] | SS2013-75 pp.19-24 |
| ET | 2012-11-17 11:15 |
佐賀 | 佐賀大学（本庄キャンパス） | Mizarによる大学数学向け高度遠隔教育用コンテンツ開発 ○井戸貴也・岡崎裕之・山崎 浩・師玉康成（信州大） ET2012-55 |
Mizar プロジェクトとは，形式化数学記述言語を用いて現行の数学定理とその証明を形式化記述し，計算機 で自動検証可能... [more] |
ET2012-55 pp.13-17 |
| ISEC, LOIS (共催) |
2011-11-14 15:35 |
大阪 | 大阪電気通信大学 | Mizarによる数論アルゴリズムの形式化と検証 ○青木祥希・岡崎裕之・師玉康成（信州大） ISEC2011-44 LOIS2011-38 |
本稿では数論アルゴリズムからユークリッドの互除法と拡張ユークリッドの互除法を取り上げ， プルーフチェッカMizarを用... [more] |
ISEC2011-44 LOIS2011-38 pp.69-74 |
| ISEC, LOIS (共催) |
2011-11-15 14:15 |
大阪 | 大阪電気通信大学 | EUC安全なメッセージ認証のためのmulti-messageプロトコルに対する記号的基準 ○鈴木斎輝・吉田真紀・藤原 融（阪大） ISEC2011-57 LOIS2011-51 |
暗号プロトコルがEUC安全であるとは, 任意のプロトコルと結合・情報共有した形で実行しても, そのプロトコルの機... [more] |
ISEC2011-57 LOIS2011-51 pp.155-162 |
| ICSS | 2011-03-25 13:25 |
東京 | 開催中止 | インターネットにおける隠蔽通信路の可能性とその検証についての一考察 ○室田朋樹（東大）・キン ティーダ ラット（北陸先端大）・堀場勝広（慶大）・櫨山寛章（奈良先端大）・加藤 朗（慶大） ICSS2010-60 |
インターネットの社会インフラ化により、ネットワーク機器の安全性検証への関心が高まっている。一般に ソフトウェアの安全性... [more] |
ICSS2010-60 pp.23-28 |
| ISEC, IT, WBS (共催) |
2011-03-04 15:45 |
大阪 | 大阪大学 | Static Adversaryに対してEUC安全な認証の記号的基準について ○鈴木斎輝・吉田真紀・藤原 融（阪大） IT2010-129 ISEC2010-133 WBS2010-108 |
暗号プロトコルがEUC安全であるとは, 任意のプロトコルと結合・情報共有した形で実行しても, そのプロトコルの機能が損な... [more] | IT2010-129 ISEC2010-133 WBS2010-108 pp.403-410 |
| VLD | 2010-03-12 13:30 |
沖縄 | 沖縄県男女共同参画センター | 順序回路の形式的検証におけるフォールスネガティブ削減のための回路変換 ○尾野紀博・中村一博・高木一義・高木直史（名大） VLD2009-125 |
本研究では、 回路変換を行うことにより、本来初期状態から到達不能であるため仕様違反ではない動作を誤検出されないように変更... [more] | VLD2009-125 pp.157-162 |
| MSS | 2009-06-03 16:50 |
大阪 | 摂南大学大阪センター | ［招待講演］確率時間CEGAR ○森下 篤・駒形龍太・山根 智（金沢大） CST2009-5 |
本論文では, 確率時間オートマトンの到達可能性解析に述語抽象化とその精錬の枠組み（CEGAR）を適用する手法を提案する.... [more] | CST2009-5 pp.25-30 |
| VLD | 2009-03-12 10:30 |
沖縄 | 沖縄県男女共同参画センター | チップ内プログラマブル配線向け形式的検証手法 ○田川貴聡・吉田浩章・藤田昌宏（東大） VLD2008-142 |
近年の開発コストの増大に伴い、FPGAに代表されるプログラマブルなデバイスの重要性が増している。このようなデバイスの重要... [more] | VLD2008-142 pp.95-100 |
| VLD, CPSY, RECONF, IPSJ-SLDM (共催) |
2009-01-30 09:05 |
神奈川 | 慶応義塾大学(日吉) | 仕様から自動生成されたプロパティによるプロトコル変換機の形式的検証手法 ○高 飛・西原 佑・松本剛史・藤田昌宏（東大） VLD2008-110 CPSY2008-72 RECONF2008-74 |
近年、設計期間を短縮するために設計資産の再利用がよく行われている。その際、異なるインタフェースを持つ設計同士を接続する場... [more] | VLD2008-110 CPSY2008-72 RECONF2008-74 pp.111-116 |
| VLD, DC, IPSJ-SLDM (共催) ICD, CPM (共催) CPSY, RECONF (併催) [詳細] |
2008-11-18 13:00 |
福岡 | 北九州学術研究都市 | 内部等価点の推定によるルールベース高位検証の高精度化 ○吉田浩章・藤田昌宏（東大/JST） |
高位設計記述間のルールベース等価性検証では、内部変数の等価点を前提として静的な依存関係や制御フローに基づいて定義された等... [more] | VLD2008-78 DC2008-46 pp.109-114 |
| CAS, MSS (共催) |
2008-11-06 16:15 |
大阪 | 大阪大学 | 階層時間オートマトン群の並列動作の述語抽象化精錬検証手法 ○山崎真一・山根 智・安井雅俊（金沢大） CAS2008-50 CST2008-28 |
本論文では，並列動作する複数の階層時間オートマトンに対して有効な述語抽象化精錬を用いる検証手法を提案する．提案手法では，... [more] | CAS2008-50 CST2008-28 pp.31-36 |
| MSS | 2008-06-03 10:50 |
愛知 | 名古屋大学野依記念学術交流館 | 述語抽象化とその洗練による確率時間オートマトンの到達可能性解析手法 駒形龍太・○森下 篤・山根 智（金沢大） CST2008-5 |
本論文では, まず確率時間オートマトンについて定義を行う. そして, その上での効率的な安全性検証手法を提案する. 提案... [more] | CST2008-5 pp.1-6 |
| SS | 2008-03-03 11:25 |
長崎 | 長崎大学 | 有界モデル検査を用いた複数UML図の形式的検証 ○宮崎 仁・横川智教・佐藤貞仁・佐藤洋一郎・早瀬道芳（岡山県立大） SS2007-60 |
筆者らはこれまでに，システム開発における複数のUML図で記述された仕様を一つの状態機械としてモデル化し，モデル検査による... [more] | SS2007-60 pp.19-24 |
| COMP | 2007-04-26 14:25 |
京都 | 京都大学(桂キャンパス) | 確率時間強模倣検証アルゴリズムの実現 ○橋爪裕樹・山根 智（金沢大） COMP2007-6 |
確率時間オートマトン上での形式的検証法は，確率的動作を伴うリアルタイムシステムの検証法に有効である．また，確率時間強模倣... [more] | COMP2007-6 pp.41-48 |
| CAS, SIP, VLD (共催) |
2005-06-28 13:50 |
宮城 | 東北大学 | 算術アルゴリズム記述言語ARITHに基づく算術演算回路の形式的設計 ○渡邉裕樹・本間尚文・青木孝文（東北大）・樋口龍雄（東北工大） |
本稿では，算術アルゴリズム記述言語ARITHに基づく並列乗算器の設計について述べる．ARITHで記述された乗算アルゴリズ... [more] | CAS2005-21 VLD2005-32 SIP2005-45 pp.37-42 |
[研究会発表申込システムのトップページに戻る]