Show simple item record

dc.contributor.advisorYang, Guowei
dc.contributor.authorWen, Junye ( )
dc.date.accessioned2018-09-19T17:25:02Z
dc.date.available2018-09-19T17:25:02Z
dc.date.issued2017-05
dc.identifier.citationWen, Ju. (2017). Distributed symbolic execution for property checking (Unpublished thesis). Texas State University, San Marcos, Texas.
dc.identifier.urihttps://digital.library.txstate.edu/handle/10877/7730
dc.description.abstractSymbolic execution is a powerful technique for checking properties in the form of assertions. It can systematically explore the program’s state space to find paths to assertion violations, and provide users with a counterexample for each violation by solving the corresponding path condition using the underlying constraint solver. However, conventional symbolic execution is configured either to explore all the state space to find all possible assertion violations, or to stop when it finds the first assertion violation. In the former case, one symbolic execution run could take a long time before giving any result, and users have to wait for the whole execution time before they could take any action to deal with the potential problems in their code. In the latter case, users need to run symbolic execution for multiple times to check all assertion violations. In this thesis, we develop a novel technique to check assertions in parallel using symbolic execution. Our technique improves the efficiency of assertion checking using symbolic execution and gives users earlier results. This technique is in two stages: in the first stage, a worker is launched to find feasible paths to the checked assertions, then in the second stage, multiple workers are launched to check assertions on these paths in parallel simultaneously, each worker focusing on one of these feasible paths. We evaluate our technique using experiments with four Java subjects, and the experimental results show its effectiveness and efficiency.
dc.formatText
dc.format.extent54 pages
dc.format.medium1 file (.pdf)
dc.language.isoen
dc.subjectSymbolic execution
dc.subjectProperty checking
dc.subjectParallel algorithm
dc.subject.lcshSoftware engineeringen_US
dc.subject.lcshComputer software--Testingen_US
dc.titleDistributed Symbolic Execution For Property Checking
txstate.documenttypeThesis
dc.contributor.committeeMemberChen, Xiao
dc.contributor.committeeMemberPodorozhny, Rodion
thesis.degree.departmentComputer Science
thesis.degree.disciplineSoftware Engineeringen_US
thesis.degree.grantorTexas State Universityen_US
thesis.degree.levelMasters
thesis.degree.nameMaster of Science
txstate.departmentComputer Science


Download

Thumbnail

This item appears in the following Collection(s)

Show simple item record