Show simple item record

dc.contributor.authorBerzish, Murphy 17:07:59 (GMT) 17:07:59 (GMT)
dc.description.abstractSatisfiability Modulo Theories (SMT) solvers supporting rich theories of strings have facilitated numerous industrial applications with the need to reason about string operations and predicates that are present in many popular programming languages. Constraints encountered in practical applications have immense value in inspiring new algorithms and heuristics that string solvers can take advantage of to tackle new, more difficult problems. This is especially relevant as the combinations of operators typically supported by string solvers, or that are encountered in program analysis constraints, quickly result in theories whose satisfiability problems are undecidable. I present a number of theoretical and practical contributions in the domain of string solving. On the theoretical side, I illustrate decidability and undecidability results related to different relevant theories which include strings. On the practical side, I describe a collection of algorithms and heuristics designed to address challenges encountered in applications of string solvers, culminating with the introduction of Z3str4, a state-of-the-art solver for theories over strings. Z3str4 incorporates many improvements over its predecessor Z3str3, including an algorithm selection architecture that takes advantage of multiple solving algorithms in order to leverage the strengths of diverse string solving procedures against formulas they are predicted to be able to solve efficiently. I also present a back-end model construction algorithm for Z3str4 which is a hybrid between word-based and unfolding-based algorithms. Furthermore, I showcase the power of Z3str4 against other state-of-the-art tools in an empirical evaluation over a large and diverse collection of benchmarks. Additionally, I describe algorithms and heuristics specific to solving regular expression constraints, and demonstrate their effectiveness in a detailed and focused empirical evaluation.en
dc.publisherUniversity of Waterlooen
dc.subjectstring solversen
dc.subjectSMT solversen
dc.subjectregular expressionsen
dc.subjectword equationsen
dc.titleZ3str4: A Solver for Theories over Stringsen
dc.typeDoctoral Thesisen
dc.pendingfalse and Computer Engineeringen and Computer Engineeringen of Waterlooen
uws-etd.degreeDoctor of Philosophyen
uws.contributor.advisorGanesh, Vijay
uws.contributor.affiliation1Faculty of Engineeringen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages