| 電子情報通信学会 研究会発表申込システム 研究会 開催スケジュール |
技報閲覧サービス [ログイン] 技報アーカイブ |
すべての研究会開催スケジュール (検索条件: すべての年度)
| 研究会 | 発表日時 | 開催地 | タイトル・著者 | 抄録 | 資料番号 | |
| VLD | 2014-03-05 15:45 |
沖縄 | 沖縄県青年会館 | VerilogHDLによるハードウェア設計への記号モデル検査の適用事例 ○横川智教・東山大地（岡山県立大）・近藤真史（川崎医療福祉大）・佐藤洋一郎・有本和民（岡山県立大）  VLD2013-166 |
従来のランダムテストによるIP検証では，検証の網羅性を保証することが極めて困難であることから，モデル検査による形式的検証... [more] | VLD2013-166 pp.177-182 |
| SS, MSS (共催) |
2014-01-31 09:55 |
愛知 | 豊田中央研究所 | CISC型組込みアセンブリプログラムのSMTベースの有界モデル検査 ○竹下 淳・小橋潤平・山根 智（金沢大） MSS2013-62 SS2013-59 |
本研究では, 組込みシステム向けアセンブリプログラムのコードブロックを対象とした,SMT有界モデル検査手法による性質検証... [more] | MSS2013-62 SS2013-59 pp.65-70 |
| IN, NV (併催) |
2013-07-19 15:15 |
北海道 | 北海道大学 工学部アカデミックラウンジ3 | 記号実行によるパケットの抽象化を用いたOpenFlowネットワークのモデル検査方式の提案 ○八鍬 豊・富沢伸行・登内敏夫（NEC） IN2013-54 |
OpenFlowネットワークに対し，モデル検査を用いて転送ループ等の不具合の有無を検証する方式を提案する．モデル検査では... [more] | IN2013-54 pp.107-112 |
| KBSE | 2013-03-15 11:25 |
東京 | 芝浦工業大学 | アーキテクチャに基づく検証ケースの提案 ○山本修一郎（名大） KBSE2012-82 |
システムの妥当性を形式手法だけで検証することは実践的ではない．このため形式手法と，テストやレビュなどとの組み合わせを明確... [more] | KBSE2012-82 pp.79-83 |
| DC | 2012-12-14 17:00 |
福井 | アオッサ(福井) | SMTソルバによる単線自動閉そく装置の検証 ○寺田夏樹（鉄道総研） DC2012-79 |
形式手法によりプログラム仕様の品質を向上させることが期待されている．仕様の検証に関して，定理証明を使用する手法は，厳密な... [more] | DC2012-79 pp.31-36 |
| SS, IPSJ-SE (連催) |
2012-11-01 13:15 |
広島 | 広島市立大学、講堂 小ホール | ネットワークの振る舞いに依存するシステムへの形式的手法の適用の検討 ○吉田信明（京都高度技研）・張 漢明・沢田篤史（南山大）・中村行宏（京都高度技研） SS2012-39 |
無線などの通信機能を持つデバイスを分散配置し，そのデバイスを通じてエリア内を移動する利用者の端末にサービス提供するシステ... [more] | SS2012-39 pp.35-40 |
| MSS | 2012-03-09 13:00 |
東京 | JAIST東京サテライト | コンシェルジュサーバを持つ電話システムの形式的検証 黒野恵人・前田 彩・○河辺義信（愛知工大） MSS2011-84 |
電話による詐欺から身を守るには，発信者が詐欺師でないことを確認することが重要である． 山本らは，この確認作業を(半)自... [more] |
MSS2011-84 pp.61-66 |
| 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 |
| KBSE | 2011-11-11 13:20 |
長野 | 信州大学工学部 | UMLモデルからの変換によるWebアプリケーションの形式検証 ○大須賀隆彦（早大）・小野康一（日本IBM）・深澤良彰（早大） KBSE2011-49 |
モデル検査法がアプリケーションソフトウェアの形式検証のために適用されつつある．ソフトウェア開発の上流工程ではモデルを開発... [more] | KBSE2011-49 pp.79-84 |
| SS | 2011-10-28 11:45 |
石川 | 北陸先端科学技術大学院大学 | 分離論理を用いたTOPPERS/ASPの割込み動作に対する検証 ○中島 崇・結縁祥治（名大） SS2011-37 |
本研究では，TOPPERS/ASPの割込み処理におけるARMアセンブリ言語コードの振舞を分離論理を用いて検証する．ARM... [more] | SS2011-37 pp.61-66 |
| SS | 2011-06-30 11:30 |
海外 | 高麗大(韓国) | An Introduction of a Formal Method in PBL: A Case Report ○Shinya Yamada・Tomohiro Iwamoto・Tsunayuki Shinozawa・Mitsuhide Honda・Ryo Miyashita（Kyushu Univ.）・Takashi Iwasaki・Yasuo Inoue（FUJITSU QNET）・Keijiro Araki・Shigeru Kusakabe・Yoichi Omori（Kyushu Univ.） SS2011-3 |
[more] | SS2011-3 pp.11-16 |
| 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 |
| SWIM | 2010-11-19 15:25 |
東京 | 東海大学（高輪） | 時間制約を含むUMLシーケンス図の検証手法 ○安田佳宏・新川芳行（龍谷大） SWIM2010-23 |
ソフトウェアの仕様検証は，構造や機能に焦点を当てた静的検証，振る舞いに焦点を当てた動的検証，そして時間制約の検証が独立に... [more] | SWIM2010-23 pp.39-44 |
| MSS | 2010-08-02 14:25 |
石川 | 金沢学院大 サテライト教室 | OTS/CafeOBJ法に基づく並行システムの実装とテスト生成 ○清野貴博（産総研）・中村正樹（金沢大） CST2010-33 |
形式仕様によるシステムの記述と、プログラミング言語によるソフトウェアの実装には隔たりがあるが、これを克服するために、筆者... [more] | CST2010-33 pp.7-12 |
| 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 |
| SS, KBSE (共催) |
2009-05-22 10:00 |
秋田 | 秋田大学 手形キャンパス | 形式的手法によるWebアプリケーションのモデル化と検証 ○本間 圭（宮城大）・高橋 薫（仙台電波高専）・富樫 敦（宮城大） SS2009-8 KBSE2009-8 |
オンライントランザクションを扱うWebアプリケーションの数は年々増加している．しかし，Webアプリケーションの設計に対す... [more] | SS2009-8 KBSE2009-8 pp.43-48 |
| VLD | 2009-03-12 10:30 |
沖縄 | 沖縄県男女共同参画センター | チップ内プログラマブル配線向け形式的検証手法 ○田川貴聡・吉田浩章・藤田昌宏（東大） VLD2008-142 |
近年の開発コストの増大に伴い、FPGAに代表されるプログラマブルなデバイスの重要性が増している。このようなデバイスの重要... [more] | VLD2008-142 pp.95-100 |
[研究会発表申込システムのトップページに戻る]