title: "HAMPI: A Solver for Word Equations over Strings, Regular Expressions and Context-free Grammars"
authors: Adam Kiezun, Vijay Ganesh, Shay Artzi, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst
venue: ACM Transactions of Software Engineering Methodology (TOSEM)
year: 2012

tweet: HAMPI is a constraint solver for strings that makes automatic bug-finding tools more efficient

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.
  <br/><br/>
  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.
  <br/><br/>
  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 <a href="http://people.csail.mit.edu/akiezun/hampi/">http://people.csail.mit.edu/akiezun/hampi</a>.

bibtex: >
  @article{KiezunHampi2012,
     author = {Adam Kiezun 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}
  }