Workshop on Theory and Practice of String Solving (TPSS)

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.

Practitioners can benefit greatly by learning about novel theoretical advances related to fragments of theories over strings, while theorists can benefit by learning about the characteristics of the various kinds of formulas generated by applications.

Program Committee

• Tevfik Bultan (Santa Barbara, USA)
• Joel Day (Loughborough, UK)
• Volker Diekert (Stuttgart, Germany)
• Stepan Holub (Prague, Czech Republic)
• Anthony Lin (Kaiserslautern, Germany)
• Vijay Ganesh, co-chair (Waterloo, Canada)
• Dirk Nowotka, co-chair (Kiel, Germany)
• Philipp Rümmer (Uppsala, Sweden)
• Margus Veanes (Microsoft Research, USA)