InSPeCT: Iterated local search for solving path conditions

Automated test case generation is attractive as it can reduce developer workload. To generate test cases, many Symbolic Execution approaches first produce Path Conditions (PCs), a set of constraints, and pass them to a Satisfiability Modulo Theories (SMT) solver. Despite numerous prior studies, auto...

Full description

Saved in:
Bibliographic Details
Main Authors: CHEN, Fuxiang, GUNAWAN, Aldy, LO, David, KIM, Sunghun
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2019
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/4521
https://ink.library.smu.edu.sg/context/sis_research/article/5524/viewcontent/Inspect_CASE_2019_av.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-5524
record_format dspace
spelling sg-smu-ink.sis_research-55242020-04-29T08:40:52Z InSPeCT: Iterated local search for solving path conditions CHEN, Fuxiang GUNAWAN, Aldy LO, David KIM, Sunghun Automated test case generation is attractive as it can reduce developer workload. To generate test cases, many Symbolic Execution approaches first produce Path Conditions (PCs), a set of constraints, and pass them to a Satisfiability Modulo Theories (SMT) solver. Despite numerous prior studies, automated test case generation by Symbolic Execution is still slow, partly due to SMT solvers’ high computationally complexity. We introduce InSPeCT, a Path Condition solver, that leverages elements of ILS (Iterated Local Search) and Tabu List. ILS is not computational intensive and focuses on generating solutions in search spaces while Tabu List prevents the use of previously generated infeasible solutions. InSPeCT is evaluated against two state-of-the-art solvers, MLB and Z3, on ten Java subject programs of varying size and complexity. The results show that InSPeCT is able to solve 16% more PCs than MLB and 41% more PCs than Z3. On average, it is 103 and 5 times faster than Z3 and MLB, respectively. It also generates tests with higher test coverage than both MLB and Z3. 2019-08-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4521 info:doi/10.1109/COASE.2019.8843039 https://ink.library.smu.edu.sg/context/sis_research/article/5524/viewcontent/Inspect_CASE_2019_av.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Iterated Local search Path condition Automated test case generation Infeasible solutions Computer Sciences Databases and Information Systems Theory and Algorithms
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Iterated Local search
Path condition
Automated test case generation
Infeasible solutions
Computer Sciences
Databases and Information Systems
Theory and Algorithms
spellingShingle Iterated Local search
Path condition
Automated test case generation
Infeasible solutions
Computer Sciences
Databases and Information Systems
Theory and Algorithms
CHEN, Fuxiang
GUNAWAN, Aldy
LO, David
KIM, Sunghun
InSPeCT: Iterated local search for solving path conditions
description Automated test case generation is attractive as it can reduce developer workload. To generate test cases, many Symbolic Execution approaches first produce Path Conditions (PCs), a set of constraints, and pass them to a Satisfiability Modulo Theories (SMT) solver. Despite numerous prior studies, automated test case generation by Symbolic Execution is still slow, partly due to SMT solvers’ high computationally complexity. We introduce InSPeCT, a Path Condition solver, that leverages elements of ILS (Iterated Local Search) and Tabu List. ILS is not computational intensive and focuses on generating solutions in search spaces while Tabu List prevents the use of previously generated infeasible solutions. InSPeCT is evaluated against two state-of-the-art solvers, MLB and Z3, on ten Java subject programs of varying size and complexity. The results show that InSPeCT is able to solve 16% more PCs than MLB and 41% more PCs than Z3. On average, it is 103 and 5 times faster than Z3 and MLB, respectively. It also generates tests with higher test coverage than both MLB and Z3.
format text
author CHEN, Fuxiang
GUNAWAN, Aldy
LO, David
KIM, Sunghun
author_facet CHEN, Fuxiang
GUNAWAN, Aldy
LO, David
KIM, Sunghun
author_sort CHEN, Fuxiang
title InSPeCT: Iterated local search for solving path conditions
title_short InSPeCT: Iterated local search for solving path conditions
title_full InSPeCT: Iterated local search for solving path conditions
title_fullStr InSPeCT: Iterated local search for solving path conditions
title_full_unstemmed InSPeCT: Iterated local search for solving path conditions
title_sort inspect: iterated local search for solving path conditions
publisher Institutional Knowledge at Singapore Management University
publishDate 2019
url https://ink.library.smu.edu.sg/sis_research/4521
https://ink.library.smu.edu.sg/context/sis_research/article/5524/viewcontent/Inspect_CASE_2019_av.pdf
_version_ 1770574882969485312