Abstract String Domain Defined with Word Equations as a Reduced Product (Extended Version)
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908589214400512 |
|---|---|
| author | Nepeivoda, Antonina Afanasyev, Ilya |
| author_facet | Nepeivoda, Antonina Afanasyev, Ilya |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_11007 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Abstract String Domain Defined with Word Equations as a Reduced Product (Extended Version) Nepeivoda, Antonina Afanasyev, Ilya Programming Languages Formal Languages and Automata Theory 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. |
| title | Abstract String Domain Defined with Word Equations as a Reduced Product (Extended Version) |
| topic | Programming Languages Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2510.11007 |