| 電子情報通信学会 研究会発表申込システム 研究会 開催スケジュール |
技報閲覧サービス [ログイン] 技報アーカイブ |
すべての研究会開催スケジュール (検索条件: すべての年度)
| 研究会 | 発表日時 | 開催地 | タイトル・著者 | 抄録 | 資料番号 | |
| SS | 2023-03-15 09:30 |
沖縄 | 名護市産業支援センター （ハイブリッド開催，主：現地開催，副：オンライン開催） |
ビットベクトル制約付き項書換え系の停止性証明のための多項式解釈プロセッサについて ○松見歩佳・西田直樹・小嶋美咲・申 東訓（名大）  SS2022-61 |
ビットベクトル制約付き項書換え系（BV-LCTRS）はC言語などのプログラムのモデルとして有用である．等価性検証に書換え... [more] | SS2022-61 pp.85-90 |
| SS | 2020-03-04 15:10 |
沖縄 | てんぶす那覇 （開催中止，技報発行あり） |
排他制御を含むプログラムから論理制約付き項書換え系への変換 ○小嶋美咲・西田直樹・松原 豊・酒井正彦（名大） SS2019-46 |
計算モデルである論理制約付き項書換え系（LCTRS）をプログラムの検証に用いる先行研究では，逐次実行される命令型プログラ... [more] | SS2019-46 pp.31-36 |
| DC, SS (共催) |
2019-10-24 14:55 |
熊本 | 熊本大学 | 存在限量子付き等式を証明するための書換え帰納法の拡張 ○西江一志・西田直樹・酒井正彦（名大） SS2019-17 DC2019-45 |
本稿では，等式を証明するための書換え帰納法を存在限量子付き等式を証明できるように拡張する．具体的にはまず，論理制約付き項... [more] | SS2019-17 DC2019-45 pp.25-30 |
| SS | 2016-03-10 11:15 |
沖縄 | 沖縄県立宮古青少年の家 | 拡張Farkas補題の部分適用による非線形ループ不変式生成を用いたプログラム検証 ○柳澤真志・西田直樹・酒井正彦（名大） SS2015-81 |
ループ不変式を生成するための手法として，与えたテンプレートと事前条件と事後条件から得られる検証式をFarkas補題に基づ... [more] | SS2015-81 pp.31-36 |
| MSS, CAS (共催) IPSJ-AL (連催) [詳細] |
2015-11-20 14:20 |
鹿児島 | 指宿市民会館 大会議室 | 分散アルゴリズムの実行列からプログラム合成とそのプログラム検証 ○山根 智（金沢大） CAS2015-50 MSS2015-24 |
分散システムの分散問題を解決する分散アルゴリズムはクラウドコンピュータやP2Pなどで多数動作しており, その正当性検証は... [more] | CAS2015-50 MSS2015-24 pp.35-40 |
| MSS | 2015-03-06 10:25 |
石川 | ITビジネスプラザ武蔵 | 割込み遷移削減手法を導入した組込みアセンブリコード向けSMTベースモデル検査器の開発 ○小橋潤平・竹下 淳・山根 智・櫻井孝平（金沢大） MSS2014-100 |
近年の発展を続けている組込みシステムにおいて, ハードウェアに依存する性質を持つソフトウェアが用いられており, 開発期間... [more] | MSS2014-100 pp.53-58 |
| SS, MSS (共催) |
2012-01-26 14:15 |
高知 | 高知市文化プラザかるぽーと | 関数呼び出しを持つプログラムの非線形ループ不変式の自動生成 ○鈴木英一・坂部俊樹・酒井正彦・草刈圭一朗・西田直樹（名大） MSS2011-61 SS2011-46 |
プログラム検証において，ループ実行中に常に成り立つ論理式である不変式が重要な役割を持っている．しかし，検証に有効なループ... [more] | MSS2011-61 SS2011-46 pp.39-44 |
| SS | 2011-03-08 09:25 |
沖縄 | 沖縄県青年会館 | プログラム変換を用いたポインタ操作プログラムの検証にむけて ～ Morrisの二分木走査アルゴリズムによるケーススタディ ～ ○渡部卓雄・森口草介・山田一宏・西崎真也（東工大） SS2010-69 |
ポインタ書き換えを伴うプログラムのプログラム変換にもとづく検証のケーススタディとして， Morrisの二分木走査アルゴ... [more] |
SS2010-69 pp.97-102 |
| SS | 2010-10-15 11:00 |
岩手 | 岩手県立大学 | 等式理論を法とするDPLL遷移系について ○馬場達也・坂部俊樹・西田直樹・草刈圭一朗・酒井正彦（名大） SS2010-36 |
SMTソルバは，指定された述語理論の下で論理式の充足可能性判定を行うツールであり，配列，リスト，キューなどの多くの理論を... [more] | SS2010-36 pp.49-54 |
| KBSE, SS (共催) |
2008-05-29 13:30 |
宮崎 | 宮崎市民プラザ 大会議室 | プレスブルガー文付き項書換え系における書換え帰納法について ○坂田 翼・西田直樹・坂部俊樹・酒井正彦・草刈圭一朗（名大） SS2008-1 KBSE2008-1 |
手続き型プログラムを等価な制約付き項書換え系に変換してプログラム等価性を検証する手法の研究において， 潜在帰納法と呼ば... [more] |
SS2008-1 KBSE2008-1 pp.1-6 |
[研究会発表申込システムのトップページに戻る]