| 電子情報通信学会 研究会発表申込システム 研究会 開催スケジュール |
技報閲覧サービス [ログイン] 技報アーカイブ |
すべての研究会開催スケジュール (検索条件: すべての年度)
| 研究会 | 発表日時 | 開催地 | タイトル・著者 | 抄録 | 資料番号 | |
| KBSE | 2024-03-15 13:20 |
沖縄 | 沖縄県総合福祉センター （ハイブリッド開催，主：現地開催，副：オンライン開催） |
可変性モデル分割手法の改善 ○岸 知二（早大）  KBSE2023-87 |
可変性モデルの解析や検証は論理に基づいて行われることが多いが，可変性モデルの持つ構成数は組み合わせ的になりうるためスケー... [more] | KBSE2023-87 pp.120-125 |
| RCC, ISEC, IT, WBS (共催) |
2024-03-14 15:30 |
大阪 | 大阪大学吹田キャンパス | トランスポートレイヤセキュリティプロトコルの形式検証の動向と課題 ○櫻田英樹（NTT/九大）・櫻井幸一（九大/ATR） IT2023-121 ISEC2023-120 WBS2023-109 RCC2023-103 |
webサーバとクライアントの間の通信では、これを安全に行うためにTLSプロトコルを用いられており、安全性のために不可欠と... [more] | IT2023-121 ISEC2023-120 WBS2023-109 RCC2023-103 pp.287-293 |
| VLD, HWS, ICD (共催) |
2024-03-02 12:05 |
沖縄 | 沖縄県男女共同参画センター【てぃるる】会議室１・２・３ （ハイブリッド開催，主：現地開催，副：オンライン開催） |
GF(2^m)上の算術演算順序回路の計算機代数に基づく形式検証に関する検討 ○迫田一歩（SCU/神戸大）・植村泰佳（SCU）・本間尚文（東北大） VLD2023-140 HWS2023-100 ICD2023-129 |
本稿では，計算機代数に基づく算術演算回路の形式的検証手法について述べる．これまで，ガロア体GF(2^m)上の算術演算回路... [more] | VLD2023-140 HWS2023-100 ICD2023-129 pp.215-220 |
| KBSE, SC (共催) |
2023-11-17 15:30 |
宮城 | 仙都会館 | スケーラビリティ改善のための可変性モデル分割について ○岸 知二（早大） KBSE2023-37 SC2023-20 |
可変性モデルを利用して論理に基づく解析や検証が行われているが，バリエーションの数は組み合わせ的になるため，近年のシステム... [more] | KBSE2023-37 SC2023-20 pp.31-36 |
| KBSE | 2023-03-17 14:35 |
広島 | JMS アステールプラザ（広島） （ハイブリッド開催，主：現地開催，副：オンライン開催） |
SimulinkとSMTソルバの連携による協調解析支援ツールの開発 ○エンジリスタ アナック ノルマン・上田賀一（茨城大） KBSE2022-67 |
協調解析で多様なモデルを対象とするには，演算や型の特性に応じてSMT ソルバを選択できる必要がある．そのため，本研究では... [more] | KBSE2022-67 pp.79-84 |
| ITS, IEE-ITS (連催) |
2021-03-15 15:05 |
ONLINE | オンライン開催 | モデル検査を用いたラウンドアバウトにおける交通量制御方式の検証 ○土屋達弘（阪大）・大塚敏史（日立） ITS2020-43 |
本研究では，形式検証手法であるモデル検査を用いて，ラウンドアバウト型の交差点における車両の交通を制御する方法の検証を行っ... [more] | ITS2020-43 pp.41-44 |
| NS, ICM, CQ, NV (併催) |
2020-11-27 11:45 |
ONLINE | オンライン開催 | システムの性質を検証可能な認証システム用フレームワークの提案 ○堀井基史・清水智弘（富士通研）・今井悟史（富士通） CQ2020-58 |
様々な手続きのデジタル化に伴い，様々な認証に関するインシデントが多発している．インシデントの発生を防止する技術として，多... [more] | CQ2020-58 pp.62-65 |
| 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 |
| ISEC, SITE, ICSS, EMM, HWS, BioX (共催) IPSJ-CSEC, IPSJ-SPT (共催) (連催) [詳細] |
2019-07-23 13:10 |
高知 | 高知工科大学 | ガロア体算術に基づく暗号ハードウェアの形式的トロイフリー性検証 ○伊東 燦・上野 嶺・本間尚文（東北大） ISEC2019-26 SITE2019-20 BioX2019-18 HWS2019-21 ICSS2019-24 EMM2019-29 |
本稿では，暗号ハードウェアにハードウェアトロイ (HT: Hardware Trojan)が含まれないことを論理的に保証... [more] | ISEC2019-26 SITE2019-20 BioX2019-18 HWS2019-21 ICSS2019-24 EMM2019-29 pp.133-138 |
| SS | 2019-03-04 17:10 |
沖縄 | 沖縄産業支援センター | ハイブリッドシステムの安全検証に向けた形式的なSTAMPモデルの提案 ○辻 光顕・高井利憲（奈良先端大）・片平真史・石濱直樹（JAXA）・柿本和希・飯田 元（奈良先端大） SS2018-67 |
自動運転車や人工衛星などの宇宙機に用いられるシステムには高い安全性が要求される。近年、このようなシステムに対する安全分析... [more] | SS2018-67 pp.91-96 |
| MSS, CAS (共催) IPSJ-AL (連催) [詳細] |
2018-11-13 15:15 |
静岡 | 熱海伊豆山温泉 ハートピア熱海 | 代数仕様を用いた数理計画モデルの形式的検証について ○中村正樹・榊原一紀（富山県立大） CAS2018-76 MSS2018-52 |
最適化ソルバーを数理計画モデルに適用するためには，ソルバーが適用可能な形式にモデル化する必要がある．本研究では，与えられ... [more] | CAS2018-76 MSS2018-52 pp.127-130 |
| VLD | 2016-02-29 13:30 |
沖縄 | 沖縄県青年会館 | Verilog-HDLによる大規模ハードウェア設計の検証支援ツールの開発 ○森光勇太・横川智教（岡山県立大）・近藤真史・宮崎 仁（川崎医療福祉大）・佐藤洋一郎・有本和民（岡山県立大）・吉田則裕（名大） VLD2015-111 |
本稿では，Verilog-HDLで記述された大規模ハードウェア設計の検証支援ツールについて報告する． 検証には，フォー... [more] |
VLD2015-111 pp.1-6 |
| KBSE, SS (共催) IPSJ-SE (連催) [詳細] |
2015-07-24 09:00 |
北海道 | 札幌市教育文化会館 | Atelier-Bによる形式検証手法の試行評価 ○山本椋太・山本修一郎（名大） SS2015-29 KBSE2015-22 |
本論文では，Bメソッドの開発ツールであるAtelier-B(CLEARSY社)を用いて実施した形式的検証手法の評価につい... [more] | SS2015-29 KBSE2015-22 pp.143-148 |
| QIT (第二種研究会) |
2015-05-25 13:20 |
大阪 | 大阪大学 | ［ポスター講演］Robertson型不確定性関係の形式的検証 増原孝昭・○栗山十織・吉田雅一・程 俊（同志社大） |
大規模な証明の正当性を検証する方法として，定理証明支援系を用いた形式的検証がある．本研究では，量子鍵配送の無条件安全性に... [more] | |
| MSS | 2015-03-06 10:25 |
石川 | ITビジネスプラザ武蔵 | 割込み遷移削減手法を導入した組込みアセンブリコード向けSMTベースモデル検査器の開発 ○小橋潤平・竹下 淳・山根 智・櫻井孝平（金沢大） MSS2014-100 |
近年の発展を続けている組込みシステムにおいて, ハードウェアに依存する性質を持つソフトウェアが用いられており, 開発期間... [more] | MSS2014-100 pp.53-58 |
| VLD, DC, IPSJ-SLDM (連催) ICD, CPM (共催) CPSY, RECONF (併催) [詳細] |
2014-11-26 10:45 |
大分 | ビーコンプラザ（別府国際コンベンションセンター） | タイミング制約を含んだ回路記述方式とその意味論 ○西村俊二・尼崎太樹・末吉敏則（熊本大） VLD2014-82 DC2014-36 |
数学的な理論に基づく厳密な検証が可能となることから，各種の形式検証手法が広がりつつあるが，その検証対象は同期回路に限られ... [more] | VLD2014-82 DC2014-36 pp.81-86 |
| RECONF | 2014-09-19 14:40 |
広島 | 杜の宿 | 様相論理によるマルチクロック同期回路の形式検証体系 ○西村俊二・尼崎太樹・末吉敏則（熊本大） RECONF2014-33 |
数学的な理論に基づく厳密な検証が可能となることから，各種の形式検証手法が広がりつつあるが，多くの場合検証対象は単一クロッ... [more] | RECONF2014-33 pp.93-98 |
| SC, IPSJ-UBI (連催) |
2014-07-28 10:00 |
東京 | 国立情報学研究所 | 異なる形式手法を用いて検査されたサービスの合成結果の検証 ○船越和大・細野 繁（NEC） SC2014-6 |
複数の形式手法を用いてそれぞれ検査されたサービスのモデルとその制約を示す論理式を入力とし，定理証明支援系であるCoq 上... [more] | SC2014-6 pp.49-54 |
| SS | 2014-03-11 10:30 |
沖縄 | てんぷす那覇：第１・２会議室 | SATソルバを活用した決定表作成・検証方式 ○伊藤信治・佐藤直人・金藤栄孝・宮崎邦彦・森 浩起・木村 誠・山口 潔（日立） SS2013-73 |
条件の組合せパターンの考慮漏れを防止する方法の１つとして、決定表の活用が有効である。しかし、決定表は、条件項目の数が多く... [more] | SS2013-73 pp.7-11 |
| SS | 2014-03-11 11:30 |
沖縄 | てんぷす那覇：第１・２会議室 | JavaにおけるequalsメソッドとhashCodeメソッドの整合性の検査手法の提案 榛葉浩章・○尾ノ上博樹・岡野浩三・楠本真二（阪大） SS2013-75 |
Javaにおいて，コレクションに格納されるオブジェクトはequalsメソッドとhashCodeメソッドをオーバーライドし... [more] | SS2013-75 pp.19-24 |
[研究会発表申込システムのトップページに戻る]