Solving string constraints lazily

13 years 3 months ago
Solving string constraints lazily
Decision procedures have long been a fixture in program analysis, and reasoning about string constraints is a key element in many program analyses and testing frameworks. Recent work on string analysis has focused on providing decision procedures that model string operations. Separating string analysis from its client applications has important and familiar benefits: it enables the independent improvement of string analysis tools and it saves client effort. We present a constraint solving algorithm for equations over string variables. We focus on scalability with regard to the size of the input constraints. Our algorithm performs an explicit search for a satisfying assignment; the search space is constructed lazily based on an automata representation of the constraints. We evaluate our approach by comparing its performance with that of existing string decision procedures. Our prototype is, on average, several orders of magnitude faster than the fastest existing implementation. Categ...
Pieter Hooimeijer, Westley Weimer
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where KBSE
Authors Pieter Hooimeijer, Westley Weimer
Comments (0)