In this paper we formalize 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 an 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 state-of-the-art approaches. We implemented a prototype of TARSIS, and we applied it to 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.

Twinning Automata and Regular Expressions for String Static Analysis / Negrini, L.; Arceri, V.; Ferrara, P.; Cortesi, A.. - 12597:(2021), pp. 267-290. ((Intervento presentato al convegno 22nd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2021 tenutosi a dnk nel 2021 [10.1007/978-3-030-67067-2_13].

Twinning Automata and Regular Expressions for String Static Analysis

Arceri V.
;
2021

Abstract

In this paper we formalize 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 an 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 state-of-the-art approaches. We implemented a prototype of TARSIS, and we applied it to 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.
Twinning Automata and Regular Expressions for String Static Analysis / Negrini, L.; Arceri, V.; Ferrara, P.; Cortesi, A.. - 12597:(2021), pp. 267-290. ((Intervento presentato al convegno 22nd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2021 tenutosi a dnk nel 2021 [10.1007/978-3-030-67067-2_13].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11381/2899272
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? ND
social impact