Title: Abstract String Domain Defined with Word Equations as a Reduced Product (Extended Version) Show Chinese title

Title: 摘要 用字方程定义的字符串域作为约简乘积（扩展版本）

Abstract: We introduce a string-interval abstract domain, where string intervals are characterized by systems of word equations (encoding lower bounds on string values) and word disequalities (encoding upper bounds). Building upon the lattice structure of string intervals, we define an abstract string object as a reduced product on a string property semilattice, determined by length-non-increasing morphisms. We consider several reduction strategies for abstract string objects and show that upon these strategies the string object domain forms a lattice. We define basic abstract string operations on the domain, aiming to minimize computational overheads on the reduction, and show how the domain can be used to analyse properties of JavaScript string manipulating programs. Show Chinese abstract

Abstract: 我们引入了一个字符串区间抽象域，其中字符串区间由单词方程系统（编码字符串值的下界）和单词不等式（编码字符串值的上界）来表征。 在字符串区间的格结构基础上，我们定义了一个抽象字符串对象，作为由长度非增同态确定的字符串属性半格上的约化乘积。 我们考虑了几种抽象字符串对象的约化策略，并证明在这些策略下，字符串对象域形成一个格。 我们在该域上定义了基本的抽象字符串操作，旨在最小化约化的计算开销，并展示了该域如何用于分析JavaScript字符串操作程序的性质。