Meeting on String Constraints and Applications
July 17 2023
Maison de la Chimie
Paris, France
Maison de la Chimie
Paris, France
String is a basic data type in almost every programming language and has been widely used in many scenarios, especially web programming. String constraint solving is a classical topic in theoretical computer science. A seminal result is the decidability of the theory of word equations shown by Makanin in 1977. String constraint solving has received much more attention in the last decade, as a result of the momentum from formal verification of string-manipulating programs. Various string constraint solvers have been developed, e.g. Z3-str3, CVC4, Norn, Trau, and Ostrich. Furthermore, various verification and testing tools, e.g. jDART for Java, Jalangi for Javascript, and PyExZ3 for Python, have been developed based on string constraint solvers.
Nevertheless, string constraint solving and formal verification of string-manipulating programs, compared to the counterpart for integer data type, are still rather immature. At first, the state-of-the-art string constraint solvers still face serious precision and scalability issues. Furthermore, formal verification techniques and tools for string manipulating programs are still in its infancy, e.g. there is few work on deductive verification and model checking for string-manipulating programs.
The primary aim of the workshop is to provide a forum for researchers with interests in string constraint solving and formal verification of string-manipulating programs to exchange ideas and techniques, aiming at fostering the fruitful research related to strings in the years next.
This workshop can be seen as a follow-up workshop of MOSCA 2019, with an emphasis on the formal verification of string manipulating programs.
Organizers
Yu-Fang Chen, Academia Sinica, TaiwanLukáš Holík, Brno University of Technology, Czechia
Zhilin Wu, Chinese Academy of Sciences, China