一句话：回顾 HAMPI——最早实用的字符串约束求解器之一——及其对字符串求解理论与应用的广泛影响。
该文是 ISSTA 2019 影响论文奖的受邀报告摘要，回顾了发表于 ISSTA 2009 的 Hampi 论文。HAMPI 是最早的一批实用字符串约束求解器之一，目标是判定字符串（字）方程、字符串操作以及正则表达式与上下文无关文法谓词构成的理论的可满足性问题。它被广泛用于解决软件工程与安全问题，并激发了大量关于字符串求解算法及其应用的研究。本文从理论与实践两方面总结字符串求解器的发展与影响。
The paper titled "Hampi: A Solver for String Constraints" was published in the proceedings of the International Symposium on Software Testing and Analysis (ISSTA) 2009, and has been selected to receive the ISSTA 2019 Impact Paper Award. The paper describes HAMPI, one of the first practical solver aimed at solving the satisfiability problem for a theory of string (word) equations, operations over strings, predicates over regular expressions and context-free grammars. HAMPI has been used widely to solve many software engineering and security problems, and has inspired considerable research on string solving algorithms and their applications.
DOI 原文 ·
@inproceedings{paperbot5356,
title = {Theory and practice of string solvers (invited talk abstract)},
author = {Adam Kiezun and Philip J. Guo and Pieter Hooimeijer and Michael D. Ernst and Vijay Ganesh},
booktitle = {ISSTA},
year = {2019},
doi = {10.1145/3293882.3338993}
}