Presenting at ATVA 2024 in Kyoto
In October 2024, I attended the 22nd International Symposium on Automated Technology for Verification and Analysis (ATVA 2024) in Kyoto, Japan. At the conference, I presented our accepted paper, “Guiding Word Equation Solving Using Graph Neural Networks.”
ATVA and APLAS 2024
ATVA 2024 took place from October 21–24, 2024. The symposium brings together researchers and practitioners working on the theoretical and practical aspects of automated analysis, verification, and synthesis, providing a forum for interaction between the international research community and industry. The conference was held in the Inamori and Yamauchi halls at Shiran-Kaikan, Kyoto University.
The conference was co-located with the 22nd Asian Symposium on Programming Languages and Systems (APLAS 2024), which focuses on programming languages and systems. The two conferences shared the venue in Kyoto and included joint activities such as the keynote on higher-order fixpoint logic for automated program verification, connecting complementary perspectives from programming languages and formal verification.
Presenting Our Word-Equation Solver
On October 24, I presented “Guiding Word Equation Solving Using Graph Neural Networks” during the Runtime Verification and Learning 2 session. The paper is joint work with Parosh Aziz Abdulla, Mohamed Faouzi Atig, Julie Cailler, and Philipp Rümmer.
Word equations are string constraints that ask whether variables can be replaced by strings so that two expressions become equal. Our work builds on the Nielsen transformation, which repeatedly splits and rewrites an equation and thereby creates a tree-shaped search space. Because the order in which branches are explored can have a major effect on solving time, we use Graph Neural Networks (GNNs) to learn which branch should be prioritized at each split point.
We introduced five graph representations for capturing the structure of word equations and implemented the resulting GNN-guided algorithm in a solver called DragonLi. The experimental evaluation covered both synthetic and real-world benchmarks. DragonLi performed particularly well on satisfiable instances: for single word equations, it solved more problems than several established string solvers, while remaining competitive on conjunctions of multiple equations.
The paper, presentation slides, BibTeX entry, and DOI record are available online.
Moments from Kyoto
