HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection

Abstract. Many automatic testing, analysis, and verification techniques for programs can effectively be 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 offthe-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, and hence researchers end up implementing their own ad-hoc solvers. Thus, there is a clear need for an effective and expressive string-constraint solver that can be easily integrated into a variety of applications. To fulfill this need, we designed and implemented H, an efficient and easyto-use string solver. Users of the H string solver specify constraints using membership predicate over regular expressions, con...

• Type: Journal
• Year: 2011
• Where: CAV
• Authors: Vijay Ganesh, Adam Kiezun, Shay Artzi, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst
• Keywords: CAV 2011, Constraint Generation, Context Free Grammars, Hardware, Source Code Documentation