Partitioning Strategies to Enhance Symbolic Execution

dc.contributor.authorMarcellino, Brendan Adrianen
dc.contributor.committeechairHsiao, Michael S.en
dc.contributor.committeememberAbbott, A. Lynnen
dc.contributor.committeememberZeng, Haiboen
dc.contributor.departmentElectrical and Computer Engineeringen
dc.date.accessioned2017-02-02T07:00:17Zen
dc.date.available2017-02-02T07:00:17Zen
dc.date.issued2015-08-11en
dc.description.abstractSoftware testing is a fundamental part of the software development process. However, testing is still costly and consumes about half of the development cost. The path explosion problem often necessitates one to consider an extremely large number of paths in order to reach a specific target. Symbolic execution can reduce this cost by using symbolic values and heuristic exploration strategies. Although various exploration strategies have been proposed in the past, the number of Satisfiability Modulo Theories (SMT) solver calls for reaching a target is still large, resulting in longer execution times for programs containing many paths. In this paper, we present two partitioning strategies in order to mitigate this problem, consequently reducing unnecessary SMT solver calls as well. In sequential partitioning, code sections are analyzed sequentially to take advantage of infeasible paths discovered in earlier sections. On the other hand, using dynamic partitioning on SSA-applied code, the code sections are analyzed in a non-consecutive order guided by data dependency metrics within the sections. Experimental results show that both strategies can achieve significant speedup in reducing the number of unnecessary solver calls in large programs. More than 1000x speedup can be achieved in large programs over conflict-driven learning.en
dc.description.degreeMaster of Scienceen
dc.format.mediumETDen
dc.identifier.othervt_gsexam:6143en
dc.identifier.urihttp://hdl.handle.net/10919/74883en
dc.publisherVirginia Techen
dc.rightsIn Copyrighten
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subjectSymbolic Executionen
dc.subjectSoftware Testingen
dc.subjectStatic Analysisen
dc.subjectPartitioning Strategiesen
dc.titlePartitioning Strategies to Enhance Symbolic Executionen
dc.typeThesisen
thesis.degree.disciplineComputer Engineeringen
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen
thesis.degree.levelmastersen
thesis.degree.nameMaster of Scienceen

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Marcellino_BA_T_2015.pdf
Size:
516.49 KB
Format:
Adobe Portable Document Format

Collections