22 July 2025 (Tuesday)
CAV 2025
University of Zagreb, Faculty of Electrical Engineering and Computing
Zagreb, Croatia

Description

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, cvc5, Norn, Trau, Ostrich, and Z3-Noodler. 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. Firstly, 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 their infancy, e.g. there are only a few works on deductive verification and model checking of 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 fruitful research related to strings in the following years.

This workshop can be seen as a follow-up workshop of MOSCA 2019 and MOSCA 2023.

Organizers

• Joel Day, Loughborough University, UK
• Matthew Hague, Royal Holloway University of London, UK
• Ondřej Lengál, Brno University of Technology, Czech Republic

Talk Proposals

We are soliciting short talk proposals. Please send your talk proposal (name, title, short abstract) to lengal@fit.vut.cz by 20 June 2025.

Confirmed Speakers (alphabetical)

• Rachel Cleaveland (Stanford University)
• Dominik D. Freydenberger (Loughborough University)
• Vojtěch Havlena (Brno University of Technology)
• Michal Hečko (Brno University of Technology)
• John Zhengyang Lu (University of Waterloo)
• Oliver Markgraf (RPTU Kaiserslautern)
• Margus Veanes (Microsoft)
• Georg Zetzsche (MPI-SWS)

Program

TBA

Venue

University of Zagreb, Faculty of Electrical Engineering and Computing
Unska ul. 3
Zagreb, Croatia