التفاصيل البيبلوغرافية
| العنوان: |
Hampi: A solver for word equations over strings, regular expressions and context-free grammar |
| المؤلفون: |
Adam Kiezun, Shay Artzi, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst |
| المساهمون: |
The Pennsylvania State University CiteSeerX Archives |
| المصدر: |
http://people.csail.mit.edu/vganesh/Publications_files/vg2011-HAMPI-TOSEM-Journal.pdfTest. |
| المجموعة: |
CiteSeerX |
| مصطلحات موضوعية: |
Categories and Subject Descriptors, D.2.7 [Software Engineering, Software Verification—Formal Methods, D.2.5 [Software Engineering, Testing and Debugging—Testing Tools General Terms, Verification, Algorithms, Reliability, Security Additional Key Words and Phrases, string constraints, word equations, regular languages, contextfree languages, concolic testing, program analysis † These authors contributed equally to this work |
| الوصف: |
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, contextfree grammars, equality/dis-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, CFG-Analyzer, and show that Hampi is several times faster. Hampi’s source code, documentation, and experimental data are available at |
| نوع الوثيقة: |
text |
| وصف الملف: |
application/pdf |
| اللغة: |
English |
| العلاقة: |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.364.6849Test; http://people.csail.mit.edu/vganesh/Publications_files/vg2011-HAMPI-TOSEM-Journal.pdfTest |
| الإتاحة: |
http://people.csail.mit.edu/vganesh/Publications_files/vg2011-HAMPI-TOSEM-Journal.pdfTest |
| حقوق: |
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| رقم الانضمام: |
edsbas.EF42EBED |
| قاعدة البيانات: |
BASE |
