I've recently stumbled across the field of Set constraints for program analysis, that is, solving equations of the form $exp_1 \subseteq exp_2$, where (depending on the particular variant of the problem), $exp_i$ is a term involving $\cup, \cap, \sim$, some set of "constructor" functions, and variables. The goal is to see if there is an assignment to the variables that satisfies the system of inclusions.

In the literature about this, the applications to program analysis are repeated over and over again, but the complexity results given seem to be abstract, and pretty removed from any realistic implementation.

For example, it's been shown that set-constraints-sat with projections are satisfiable using a variant of tree automata. A broad overview can be found in Chapter 5 of this free book

I'm wondering:

  • Are these ever used in practice, or does the $DEXPTIME$ and $NEXPTIME$-completeness of most variants mean that it's never been put to use in practice?
  • Is there any research on practical implementations of these algorithms, trying to obtain performance for typical inputs despite the complexity? Research like this is pretty common for NP-complete problems (sespecially SAT).
  • Are set constraints out-dated i.e. has program analysis moved on from them? Is looking into them a dead end?
  • 1
    $\begingroup$ I've definitely seem papers that have used set constraints to build useful program analysis tools. However, they use a more limited class of set constraints (no projections, I think?). See, e.g., work of Alex Aiken and his students. Doesn't the paper you link to give some examples (Section 1.2 and citations)? These days I have the impression that set constraints are out-dated and less popular (especially given the rise in SAT/SMT-based methods), but I'm not an expert on the subject. $\endgroup$
    – D.W.
    Commented Oct 12, 2017 at 20:39


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.