Title: A Framework for Efficient Analysis of String Constraints

Abstract: The string data type is omnipresent in all modern  programming languages.  This is especially true with  scripting languages. The verification of programs manipulating string data type is a very important and challenging problem since many security vulnerabilities such as injection and cross-site scripting attacks are often caused by malicious string inputs. Software (bounded) model checking,   symbolic execution techniques  and concolic testing  are the main approaches for  program testing and verification. Such approaches are highly based on efficient  symbolic encodings of program executions into  formulas, and rely  on highly performing constraint solvers  to reason about those encodings. 
In this keynote talk, we  will present our recent decision procedure for string constraints. We will focus on the decision procedure that uses the Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under- and an over-approximation module running in an alternating manner. The flow of information between these modules is used to increase their precision in an automatic manner. We will also discuss how Graph Neural Networks can be integrated into the framework to guide the solving process and enhance the performance of string constraint decision procedures.
This talk will be based on join work with Parosh Aziz Abdulla, Julie Cailler, Yu-Fang Chen, Bui Phi Diep, Julian Dolby, Lukas Holik, Denghang Hu, Petr Janku, Chencheng Liang, Hsin-Hung Lin, Ahmed Rezine, Philipp Rüummer, Wei-LunTsai, Wei-Cheng Wu, Zhillin Wu and Di-De Yen.