This project aims to use deep learning techniques to guide the solution process of string equation problems. String equation solving is a branch of formal methods focused on determining solutions to equations where variables represent strings, instead of traditional numerical values. Within these equations, strings may undergo operations such as concatenation, substring extraction, and pattern matching. Common applications include program analysis and database querying. The challenge arises from the combinatorial explosion in the search space. Initially, we plan to develop a basic string equation solver based on the algorithms referenced in [1] and [2]. Subsequently, we will design a deep-learning task to guide these algorithms. ------------------- We will utilize Alcis@C3SE for training the deep learning model. Rackham@UPPMAX will be employed to extract training data and evaluate the algorithm against benchmarks. -------------------- References [1] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman. Norn: An SMT Solver for String Constraints. 27th International Conference on Computer Aided Verification (CAV), 2015, San Francisco, CA, USA Springer, LNCS 9206, pages 462-469. [2] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman. String Constraints for Verification. 26th International Conference on Computer Aided Verification (CAV), 2014, Vienna, Austria Springer, LNCS 8559, pages 150-166.