HAMPI: A solver for string constraints
Submitted by mernst on Wed, 2011-11-30 14:35
| Title | HAMPI: A solver for string constraints |
| Publication Type | Miscellaneous |
| Year of Publication | 2009 |
| Authors | Kieżun A, Ganesh V, Guo PJ, Hooimeijer P, Ernst MD |
| Abstract | <p>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, if any, effective and sufficiently expressive off-the-shelf solvers for string constraints generated by analysis techniques for string-manipulating programs. </p> <p> We designed and implemented HAMPI, a solver for string constraints over bounded string variables. HAMPI constraints express membership in regular languages and bounded 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. </p> <p> 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 <a href='http://people.csail.mit.edu/akiezun/hampi/'>http://people.csail.mit.edu/akiezun/hampi/</a>.</p> |
| Downloads | HAMPI implementation PDF |
| Citation Key | KiezunGGHE2009:TR |
Last changed Mon, 2013-06-03 10:27

cs.