Non-Numerical Weakly Relational Domains
CoRR(2024)
摘要
The weakly relational domain of Octagons offers a decent compromise between
precision and efficiency for numerical properties. Here, we are concerned with
the construction of non-numerical relational domains. We provide a general
construction of weakly relational domains, which we exemplify with an extension
of constant propagation by disjunctions. Since for the resulting domain of
2-disjunctive formulas, satisfiability is NP-complete, we provide a general
construction for a further, more abstract weakly relational domain where the
abstract operations of restriction and least upper bound can be efficiently
implemented. In the second step, we consider a relational domain that tracks
conjunctions of inequalities between variables, and between variables and
constants for arbitrary partial orders of values. Examples are sub(multi)sets,
as well as prefix, substring or scattered substring orderings on strings. When
the partial order is a lattice, we provide precise polynomial algorithms for
satisfiability, restriction, and the best abstraction of disjunction.
Complementary to the constructions for lattices, we find that, in general,
satisfiability of conjunctions is NP-complete. We therefore again provide
polynomial abstract versions of restriction, conjunction, and join. By using
our generic constructions, these domains are extended to weakly relational
domains that additionally track disjunctions. For all our domains, we indicate
how abstract transformers for assignments and guards can be constructed.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要