Twinning automata and regular expressions for string static analysis
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2020
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866918384780705792 |
|---|---|
| author | Negrini, Luca Arceri, Vincenzo Ferrara, Pietro Cortesi, Agostino |
| author_facet | Negrini, Luca Arceri, Vincenzo Ferrara, Pietro Cortesi, Agostino |
| contents | In this paper we formalize and prove the soundness of Tarsis, a new abstract domain based on the abstract interpretation theory that approximates string values through finite state automata. The main novelty of Tarsis is that it works over an alphabet of strings instead of single characters. On the one hand, such approach requires a more complex and refined definition of the widening operator, and the abstract semantics of string operators. On the other hand, it is in position to obtain strictly more precise results than than state-of-the-art approaches. We implemented a prototype of Tarsis, and we applied it on some case studies taken from some of the most popular Java libraries manipulating string values. The experimental results confirm that Tarsis is in position to obtain strictly more precise results than existing analyses. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2006_02715 |
| institution | arXiv |
| publishDate | 2020 |
| record_format | arxiv |
| spellingShingle | Twinning automata and regular expressions for string static analysis Negrini, Luca Arceri, Vincenzo Ferrara, Pietro Cortesi, Agostino Software Engineering Formal Languages and Automata Theory In this paper we formalize and prove the soundness of Tarsis, a new abstract domain based on the abstract interpretation theory that approximates string values through finite state automata. The main novelty of Tarsis is that it works over an alphabet of strings instead of single characters. On the one hand, such approach requires a more complex and refined definition of the widening operator, and the abstract semantics of string operators. On the other hand, it is in position to obtain strictly more precise results than than state-of-the-art approaches. We implemented a prototype of Tarsis, and we applied it on some case studies taken from some of the most popular Java libraries manipulating string values. The experimental results confirm that Tarsis is in position to obtain strictly more precise results than existing analyses. |
| title | Twinning automata and regular expressions for string static analysis |
| topic | Software Engineering Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2006.02715 |