Non-numerical weakly relational domains

Helmut Seidl, Julian Erhard, Sarah Tilscher, Michael Schwarz

Research output: Contribution to journalArticlepeer-review

1 Scopus citations

Abstract

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.

Original languageEnglish
Pages (from-to)479-494
Number of pages16
JournalInternational Journal on Software Tools for Technology Transfer
Volume26
Issue number4
DOIs
StatePublished - Aug 2024

Keywords

  • 2-decomposable relational domains
  • 2-disjunctive constants
  • Directed domains
  • Weakly relational domains

Fingerprint

Dive into the research topics of 'Non-numerical weakly relational domains'. Together they form a unique fingerprint.

Cite this