Theory and practice of string solvers (invited talk abstract)
| Autor: | Vijay Ganesh, Adam Kiezun, Michael D. Ernst, Philip J. Guo, Pieter Hooimeijer |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Theoretical computer science
Computer science String (computer science) 020207 software engineering 02 engineering and technology Solver Rule-based machine translation 0202 electrical engineering electronic engineering information engineering Key (cryptography) 020201 artificial intelligence & image processing State (computer science) Regular expression Boolean satisfiability problem Word (computer architecture) |
| Zdroj: | ISSTA |
| Popis: | The paper titled "Hampi: A Solver for String Constraints" was published in the proceedings of the International Symposium on Software Testing and Analysis (ISSTA) 2009, and has been selected to receive the ISSTA 2019 Impact Paper Award. The paper describes HAMPI, one of the first practical solver aimed at solving the satisfiability problem for a theory of string (word) equations, operations over strings, predicates over regular expressions and context-free grammars. HAMPI has been used widely to solve many software engineering and security problems, and has inspired considerable research on string solving algorithms and their applications. In this talk, we review the state of research on the theory and practice of string solving algorithms, specifically highlighting key historical developments that have led to their widespread use. On the practical front, we discuss different kinds of algorithmic paradigms, such as word- and automata-based, that have been developed to solve string and regular expression constraints. We then focus on the many hardness results that theorists have proved for fragments of theories over strings. Finally, we conclude with open theoretical problems, practical algorithmic challenges, and future applications of string solvers. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|