This time in PL reading, we will discuss D3: Data-Driven Disjunctive Abstraction by H. Peleg, S. Shoham and E. Yahav.
Abstract. We address the problem of computing an abstraction for a set of examples,
which is precise enough to separate them from a set of counterexamples.
The challenge is to find an over-approximation of the positive examples that does
not represent any negative example. Conjunctive abstractions (e.g., convex numerical
domains) and limited disjunctive abstractions, are often insufficient, as
even the best such abstraction might include negative examples. One way to improve
precision is to consider a general disjunctive abstraction.
We present D3, a new algorithm for learning general disjunctive abstractions. Our
algorithm is inspired by widely used machine-learning algorithms for obtaining
a classifier from positive and negative examples. In contrast to these algorithms
which cannot generalize from disjunctions, D3 obtains a disjunctive abstraction
that minimizes the number of disjunctions. The result generalizes the positive
examples as much as possible without representing any of the negative examples.
We demonstrate the value of our algorithm by applying it to the problem of data-driven
differential analysis, computing the abstract semantic difference between
two programs. Our evaluation shows that D3 can be used to effectively learn
precise differences between programs even when the difference requires a disjunctive