お知らせ 2023年度・2024年度 学生員 会費割引キャンペーン実施中です
お知らせ 技術研究報告と和文論文誌Cの同時投稿施策(掲載料1割引き)について
お知らせ 電子情報通信学会における研究会開催について
お知らせ NEW 参加費の返金について
電子情報通信学会 研究会発表申込システム
講演論文 詳細
技報閲覧サービス
[ログイン]
技報アーカイブ
 トップに戻る 前のページに戻る   [Japanese] / [English] 

講演抄録/キーワード
講演名 2021-03-04 13:25
Software Analysis WorkbenchとSymbolicPathFindreを使用した網羅的な反例とパス制約の生成
辛島 凜小形真平岡野浩三信州大SS2020-41
抄録 (和) Software Analysis Workbench (SAW)はJVMバイトコードをシンボリック実行によってモデル化し,関数単位でモデル検査を行なうことができるツールである.
SAW用いて網羅的な反例の導出を行ない,反例の実行パスを特定するための手法としてPath-Directed Symbolic Execution (PDSE)をSAWで実行するための手法と,PDSEを改良し検証時間の短縮を図った手法であるCounter-Example Path-Directed Symbolic Execution (CEG-PDSE)を報告する.
さらに,提案手法を自動的に実行するツールを実装し,評価実験を行った結果,CEG-PDSEはPDSEに対し最大で75%実行時間を削減する有効性を示した. 
(英) Software Analysis Workbench (SAW) generates models from JVM bytecode by symbolic execution.
Users can perform model check on a function by function.
In this paper, we propose a method to perform Path-Directed Symbolic Execution (PDSE) in SAW for generating exhaustive counter-examples.
Also, we propose Counter-Example Guided Symbolic Execution (CEG-PDSE) as improvement of PDSE.
In addition, we have implemented a tool that automatically executes CEG-PDSE.
The evaluation experiment shows the effictiveness of the proposed method.
キーワード (和) SAW / SPF / JUnit / Model Checking / Symbolic Execution / / /  
(英) / / / / / / /  
文献情報 信学技報, vol. 120, no. 407, SS2020-41, pp. 78-83, 2021年3月.
資料番号 SS2020-41 
発行日 2021-02-24 (SS) 
ISSN Online edition: ISSN 2432-6380
著作権に
ついて
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034)
査読に
ついて
本技術報告は査読を経ていない技術報告であり,推敲を加えられていずれかの場に発表されることがあります.
PDFダウンロード SS2020-41

研究会情報
研究会 SS  
開催期間 2021-03-03 - 2021-03-04 
開催地(和) オンライン開催 
開催地(英) Online 
テーマ(和) 一般 
テーマ(英)  
講演論文情報の詳細
申込み研究会 SS 
会議コード 2021-03-SS 
本文の言語 日本語 
タイトル(和) Software Analysis WorkbenchとSymbolicPathFindreを使用した網羅的な反例とパス制約の生成 
サブタイトル(和)  
タイトル(英) Generating Exhaustive Counterexample and Path Constraint with Software Analysis Workbench and Symbolic PathFinder 
サブタイトル(英)  
キーワード(1)(和/英) SAW /  
キーワード(2)(和/英) SPF /  
キーワード(3)(和/英) JUnit /  
キーワード(4)(和/英) Model Checking /  
キーワード(5)(和/英) Symbolic Execution /  
キーワード(6)(和/英) /  
キーワード(7)(和/英) /  
キーワード(8)(和/英) /  
第1著者 氏名(和/英/ヨミ) 辛島 凜 / Rin Karashima / カラシマ リン
第1著者 所属(和/英) 信州大学 (略称: 信州大)
Shinshu University (略称: Shinshu Univ.)
第2著者 氏名(和/英/ヨミ) 小形 真平 / Shinpei Ogata / オガタ シンペイ
第2著者 所属(和/英) 信州大学 (略称: 信州大)
Shinshu University (略称: Shinshu Univ.)
第3著者 氏名(和/英/ヨミ) 岡野 浩三 / Kozo Okano / オカノ コウゾウ
第3著者 所属(和/英) 信州大学 (略称: 信州大)
Shinshu University (略称: Shinshu Univ.)
第4著者 氏名(和/英/ヨミ) / /
第4著者 所属(和/英) (略称: )
(略称: )
第5著者 氏名(和/英/ヨミ) / /
第5著者 所属(和/英) (略称: )
(略称: )
第6著者 氏名(和/英/ヨミ) / /
第6著者 所属(和/英) (略称: )
(略称: )
第7著者 氏名(和/英/ヨミ) / /
第7著者 所属(和/英) (略称: )
(略称: )
第8著者 氏名(和/英/ヨミ) / /
第8著者 所属(和/英) (略称: )
(略称: )
第9著者 氏名(和/英/ヨミ) / /
第9著者 所属(和/英) (略称: )
(略称: )
第10著者 氏名(和/英/ヨミ) / /
第10著者 所属(和/英) (略称: )
(略称: )
第11著者 氏名(和/英/ヨミ) / /
第11著者 所属(和/英) (略称: )
(略称: )
第12著者 氏名(和/英/ヨミ) / /
第12著者 所属(和/英) (略称: )
(略称: )
第13著者 氏名(和/英/ヨミ) / /
第13著者 所属(和/英) (略称: )
(略称: )
第14著者 氏名(和/英/ヨミ) / /
第14著者 所属(和/英) (略称: )
(略称: )
第15著者 氏名(和/英/ヨミ) / /
第15著者 所属(和/英) (略称: )
(略称: )
第16著者 氏名(和/英/ヨミ) / /
第16著者 所属(和/英) (略称: )
(略称: )
第17著者 氏名(和/英/ヨミ) / /
第17著者 所属(和/英) (略称: )
(略称: )
第18著者 氏名(和/英/ヨミ) / /
第18著者 所属(和/英) (略称: )
(略称: )
第19著者 氏名(和/英/ヨミ) / /
第19著者 所属(和/英) (略称: )
(略称: )
第20著者 氏名(和/英/ヨミ) / /
第20著者 所属(和/英) (略称: )
(略称: )
講演者 第1著者 
発表日時 2021-03-04 13:25:00 
発表時間 25分 
申込先研究会 SS 
資料番号 SS2020-41 
巻番号(vol) vol.120 
号番号(no) no.407 
ページ範囲 pp.78-83 
ページ数
発行日 2021-02-24 (SS) 


[研究会発表申込システムのトップページに戻る]

[電子情報通信学会ホームページ]


IEICE / 電子情報通信学会