Workshop on Theory and Practice of String Solving (TPSS)
Vijay Ganesh, Dirk Nowotka
Abstract: Over the last decade, there has been considerable interest on the topic of string SMT solvers by researchers working broadly in verification, security, and software engineering. Theories over strings, arithmetic, and regular expressions have several applications in the context of verification and testing of string-intensive programs, specifically, Web security. In order to satiate this intense demand, many successful string solvers such as CVC4, Z3seq, and Z3str3 have been developed. At the other end of the spectrum, for over a century now, logicians and mathematicians have been studying combinatorics over words and theories over string equations and their extensions. Unfortunately, the string practitioner and theorist rarely interact with each other. They often publish in very different kinds of venues with little overlap, with practitioners focusing on CAV, PLDI etc., while theorists publishing mostly in DLT, STACS, MFCS etc. The purpose of this proposed Theory and Practice of String Solving (TPSS) workshop is to bring practitioners and theorists together at a single CAV co-located venue and benefit from each others' expertise, currently largely siloed away.