HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars

Download: PDF, HAMPI implementation and experiments, ISSTA 2009 slides (PDF).

“HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars” by Adam Kieżun, Vijay Ganesh, Shay Artzi, Philip J. Guo, Pieter Hooimeijer, and Michael D. Ernst. ACM Transactions on Software Engineering and Methodology, vol. 21, no. 4, Nov. 2012, pp. 25:1-25:28.
A tutorial and paper appeared as “HAMPI: a string solver for testing, analysis and vulnerability detection” by Vijay Ganesh, Adam Kieżun, Shay Artzi, Philip J. Guo, Pieter Hooimeijer, and Michael D. Ernst. In CAV 2011: 23rd International Conference on Computer Aided Verification, (Snowbird, UT, USA), July 2011, pp. 1-19.
A previous version appeared as “HAMPI: A solver for string constraints” by Adam Kieżun, Vijay Ganesh, Philip J. Guo, Pieter Hooimeijer, and Michael D. Ernst. In ISSTA 2009, Proceedings of the 2009 International Symposium on Software Testing and Analysis, (Chicago, IL, USA), July 2009, pp. 105-116.
A previous version appeared as “HAMPI: A solver for string constraints” by Adam Kieżun, Vijay Ganesh, Philip J. Guo, Pieter Hooimeijer, and Michael D. Ernst. MIT Computer Science and Artificial Intelligence Laboratory technical report MIT-CSAIL-TR-2009-004, (Cambridge, MA), February 4, 2009.

Abstract

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 software reliability 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 of string-manipulating programs, so researchers end up implementing their own ad-hoc solvers.

To fulfill this need, we designed and implemented Hampi, a solver for string constraints over bounded string variables. Users of Hampi specify constraints using regular expressions, context-free grammars, equality between string terms, and typical string operations such as concatenation and substring extraction. Hampi then finds a string that satisfies all the constraints or reports that the constraints are unsatisfiable.

We demonstrate Hampi's expressiveness and efficiency by applying it to program analysis and automated testing. We used Hampi in static and dynamic analyses for finding SQL injection vulnerabilities in Web applications with hundreds of thousands of lines of code. We also used Hampi in the context of automated bug finding in C programs using dynamic systematic testing (also known as concolic testing). We then compared Hampi with another string solver, CFGAnalyzer, and show that Hampi is several times faster. Hampi's source code, documentation, and experimental data are available at https://people.csail.mit.edu/akiezun/hampi/

Download: PDF, HAMPI implementation and experiments, ISSTA 2009 slides (PDF).

BibTeX entry:

@article{KiezunGAGHE2012,
   author = {Adam Kie{\.z}un and Vijay Ganesh and Shay Artzi and Philip J.
	Guo and Pieter Hooimeijer and Michael D. Ernst},
   title = {{HAMPI}: A solver for word equations over strings, regular
	expressions, and context-free grammars},
   journal = {ACM Transactions on Software Engineering and Methodology},
   volume = {21},
   number = {4},
   pages = {25:1--25:28},
   month = nov,
   year = {2012}
}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.