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.

翻译：我们引入了一种字符串区间抽象域，其中字符串区间由字方程系统（编码字符串值的下界）和字不等式系统（编码字符串值的上界）共同刻画。基于字符串区间的格结构，我们通过在字符串属性半格上定义约简积来构建抽象字符串对象，该约简积由长度非递增态射确定。我们探讨了抽象字符串对象的多种约简策略，并证明基于这些策略的字符串对象域构成一个格结构。我们在该域上定义了基本抽象字符串操作，旨在最小化约简过程中的计算开销，并展示了如何利用该域分析JavaScript字符串操作程序的属性。