Hampi: A Solver For String Constraints
ISSTA(2009)
摘要
Many automatic testing, analysis, and verification techniques for programs can be effectively reduced to a constraint-generation phase followed by a constraint-solving phase. This separation of concerns often leads to more effective and maintainable tools. The increasing efficiency of off-the-shelf constraint solvers makes this approach even more compelling. However, there are few effective and sufficiently expressive off-the-shelf solvers for string constraints generated by analysis techniques for string-manipulating programs.We designed and implemented HAMPI, a solver for string constraints over fixed-size string variables. HAMPI constraints express membership in regular languages and fixed-size context-free languages. HAMPI constraints may contain context-free-language definitions, regular-language definitions and operations, and the membership predicate. Given a set of constraints, HAMPI outputs a string that satisfies all the constraints, or reports that the constraints are unsatisfiable. \ HAMPI is expressive and efficient, and can be successfully applied to testing and analysis of real programs. Our experiments use HAMPI in: static and dynamic analyses for finding SQL injection vulnerabilities in Web applications; automated bug finding in C programs using systematic testing; and compare HAMPI with another string solver. HAMPI'S source code, documentation, and the experimental data are available at http: //people.csail.mit.edu/akiezun/hampi.
更多查看译文
关键词
string constraints,regular languages,context-free languages
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络