related.tex

\section{Conclusions and Related Work}
The problem of creating scalable, precise, and predictable abstractions for sets remains challenging.  This paper introduced several ways of approaching this problem and showed that for symbolic set abstractions, binary decision diagrams offer good performance, precision, and predictability trade-offs.  However, it is preferable to craft a custom abstraction such as the linear abstraction.  This offers more predictable performance by only having the necessary precision.

There are other set abstractions available.
They all offer different functionality at different costs.
The QUIC graphs abstraction~\cite{ab:ecoop:13,quicr:cav:14} focuses on
combining reasoning about contents with symbolic set reasoning.
This comes at the cost of performance, precision, and predictability
when it comes to purely symbolic set reasoning.
The FixBag abstraction~\cite{fixbag:cav:11} attacks the problems of
multisets or bags offering cardinality reasoning as well as symbolic
set reasoning.
Similar to QUIC graphs, it exchanges performance, precision, and
predictability for this functionality.
The linear and the BDD-based abstractions we present here are designed
to be scalable, precise, and predictable rather than complex.

There are several decision procedures for sets.  Bradley et al.~\cite{bradley:vmcai:06} introduced a decision procedure for set contents and relationships (without cardinality).  BAPA~\cite{knr:jar:06,jahob:thesis:07} is a decision procedure for sets with cardinality.  Z3~\cite{mb:tacas:08} also includes a decision procedure for sets with contents.  None of these decision procedures are designed for invariant generation.  It is possible that interpolation procedures~\cite{interp:cav:03} could be designed based upon these procedures, but to our knowledge this has not been done.  Regardless, without invariant generation that is compatible with static analysis, it is difficult to use this work as a component of an existing analysis.

Due to the prevalence of Boolean algebra in the algorithms presented here, there is a natural correspondence to hardware model checking~\cite{mc:toplas:86} and predicate abstraction~\cite{sympred:cav:03}.  However, one significant difference is the composability of the abstractions presented here.  The equality and packing functors alter the underlying abstractions, making problems that were previously intractable, tractable.  Additionally, because these are abstract domains, there is no conflation of control flow with data flow and as a result, many of the analysis problems are changed.

Additionally, the use of BDDs is similar to \cite{mauborgne:thesis:99}, where BDDs are extended to be possibly-cyclic graphs.  These are used to represent tree structures.

%  There are several differences, however.  First, the algorithms described here are designed to be integrated with a static analyzer, whereas a hardware model checkers are not.  The big difference is that hardware model checkers combine the control flow with the data flow into one single logic system.  Here, we maintain the difference as the host static analyzer dictates how the abstract domain is used.  This means that abstract domains can only see the constraints and domain operations as they occur, whereas a hardware model checker can see the whole analysis globally.  As a result, it is difficult to apply hardware model checkers in the environments where it is possible to apply abstract domains.

As a result, we find that for now, abstractions that construct normal forms, such as the linear abstraction and binary decision diagrams, offer the best way of handling sets in static analysis.  We have shown that depending on the application, both of these techniques offer sufficient performance and precision, especially when combined with functors for performing packing and managing equalities.  The end result is that these abstractions are scalable, precise, and predictable in their behavior.