Presentation 2021-03-04
Generating Exhaustive Counterexample and Path Constraint with Software Analysis Workbench and Symbolic PathFinder
Rin Karashima, Shinpei Ogata, Kozo Okano,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) 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.
Keyword(in Japanese) (See Japanese page)
Keyword(in English)
Paper # SS2020-41
Date of Issue 2021-02-24 (SS)

Conference Information
Committee SS
Conference Date 2021/3/3(2days)
Place (in Japanese) (See Japanese page)
Place (in English) Online
Topics (in Japanese) (See Japanese page)
Topics (in English)
Chair Takashi Kobayashi(Tokyo Inst. of Tech.)
Vice Chair Kozo Okano(Shinshu Univ.)
Secretary Kozo Okano(Hiroshima City Univ.)
Assistant Shinpei Ogata(Shinshu Univ.)

Paper Information
Registration To Technical Committee on Software Science
Language JPN
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) Generating Exhaustive Counterexample and Path Constraint with Software Analysis Workbench and Symbolic PathFinder
Sub Title (in English)
Keyword(1)
Keyword(2)
Keyword(3)
Keyword(4)
Keyword(5)
1st Author's Name Rin Karashima
1st Author's Affiliation Shinshu University(Shinshu Univ.)
2nd Author's Name Shinpei Ogata
2nd Author's Affiliation Shinshu University(Shinshu Univ.)
3rd Author's Name Kozo Okano
3rd Author's Affiliation Shinshu University(Shinshu Univ.)
Date 2021-03-04
Paper # SS2020-41
Volume (vol) vol.120
Number (no) SS-407
Page pp.pp.78-83(SS),
#Pages 6
Date of Issue 2021-02-24 (SS)