講演抄録/キーワード |
講演名 |
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 |