UWSpace is currently experiencing technical difficulties resulting from its recent migration to a new version of its software. These technical issues are not affecting the submission and browse features of the site. UWaterloo community members may continue submitting items to UWSpace. We apologize for the inconvenience, and are actively working to resolve these technical issues.
 

StringFuzz: A Fuzzer for String SMT Solvers

Simple item page
dc.contributor.authorBlotsky, Dmitry
dc.date.accessioned2018-08-10T13:49:34Z
dc.date.available2018-08-10T13:49:34Z
dc.date.issued2018-08-10
dc.date.submitted2018-07-30
dc.description.abstractWe introduce StringFuzz, a software tool for automatically testing string SMT solvers. String SMT solvers are specialised software tools for solving the Satisfiability Modulo Theories (SMT) problem with string contraints, which is a type of constraint satisfaction problem applicable in industry. Like all tools, string SMT solvers need testing. The developers of solvers commonly test them with published test suites: pre-generated sets of problem instances (i.e. example problems). As new features are added to string SMT solvers, they often are not exercised by existing suites. We introduce StringFuzz, a tool for solver developers to generate SMT instances to exercise and find defects in their solvers. We describe StringFuzz’s features for generating and transforming SMT instances with string and regex constraints. We also show StringFuzz’s many controls, and show how to use them to generate specially tuned scaling instances. For public use, we present our own suite of StringFuzz-generated SMT instances. We also introduce StringBreak, an automated exploratory tester for string SMT solvers, which uses a genetic algorithm to generate SMT instances that take a long time for solvers to solve. To demonstrate the usefulness of StringFuzz and StringBreak, we show experimental results from testing leading string SMT solvers (Z3str3, CVC4, Z3str2, and Norn) with them. We describe two defects and one potential future enhancement that we discovered in Z3str3 as a result of our experiments.en
dc.identifier.urihttp://hdl.handle.net/10012/13564
dc.language.isoenen
dc.pendingfalse
dc.publisherUniversity of Waterlooen
dc.subjectsmt solversen
dc.subjectfuzzeren
dc.subjecttestingen
dc.subjectstringsen
dc.subjectsmt-liben
dc.titleStringFuzz: A Fuzzer for String SMT Solversen
dc.typeMaster Thesisen
uws-etd.degreeMaster of Applied Scienceen
uws-etd.degree.departmentElectrical and Computer Engineeringen
uws-etd.degree.disciplineElectrical and Computer Engineeringen
uws-etd.degree.grantorUniversity of Waterlooen
uws.contributor.advisorGanesh, Vijay
uws.contributor.affiliation1Faculty of Engineeringen
uws.peerReviewStatusUnrevieweden
uws.published.cityWaterlooen
uws.published.countryCanadaen
uws.published.provinceOntarioen
uws.scholarLevelGraduateen
uws.typeOfResourceTexten

Files

Original bundle
Now showing 1 - 2 of 2
No Thumbnail Available
Name:
stringfuzz.zip
Size:
208 KB
Format:
File compressed with the ZIP data compression and archival format
Description:
StringFuzz source code.
Download
Thumbnail Image
Name:
Blotsky_Dmitry.pdf
Size:
469.16 KB
Format:
Adobe Portable Document Format
Description:
The thesis, as a PDF document.
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
6.08 KB
Format:
Item-specific license agreed upon to submission
Description:
Download

Collections

Theses
Electrical and Computer Engineering