论文标题
双重自动机和正则表达式用于字符串静态分析
Twinning automata and regular expressions for string static analysis
论文作者
论文摘要
在本文中，我们基于抽象的解释理论形式化并证明了Tarsis的健全性，这是一个新的抽象领域，该域通过有限状态自动机近似弦乐值。塔西斯（Tarsis）的主要新颖性是它可以在字母的字母上而不是单个字符上工作。一方面，这种方法需要对延伸的操作员的更复杂和更精致的定义，以及字符串运算符的抽象语义。另一方面，比最先进的方法更准确地获得结果。我们实施了Tarsis的原型，并将其应用于一些操纵字符串值的最受欢迎的Java库中进行的一些案例研究。实验结果证实，与现有分析相比，Tarsis可以获得严格的更精确的结果。
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.
