We address the problem of selecting a banner advertisement, based on the profile of the online user. The profile consists of the set of webpages opened by the online user, optionally clustered. In order to select the banner, we train a classifier with a dataset containing rules of the form P(u) → B(u), where P(u) is the profile of user u, and B(u) is the set of banners clicked by user u. We present two possible transformations that we use in order to train the classifier. In the first transformation, TMax, we put only one line P(u) →b, where b is the most frequently clicked banner by the user u. In the second transformation, TMultiline, we put one line P(u) → b, for each banner b in B(u). Finally, we perform several experiments, which show that there is a strong correlation between the profiles of the user, and the banners clicked by the user.

The key to many approaches to reason about pointerbased data structures is the availability of a decision procedure to automatically discharge proof obligations in a theory encompassing data, pointers, and the reachability relation induced by pointers. So far, only approximate solutions have been proposed which abstract either the data or the reachability component. Indeed, such approximations cause a lack of precision in the verification techniques where the decision procedures are exploited. In this paper, we consider the pointer-based data structure of singly-linked lists and define a Theory of Linked Lists (TLL). The theory is expressive since it is capable of precisely expressing both data and reachability constraints, while ensuring decidability. Furthermore, its decidability problem is NP-complete. We also design a practical decision procedure for TLL which can be combined with a wide range of available decision procedures for theories in firstorder logic.

Interpolation based automatic abstraction is a powerful and robust technique for the automated analysis of hardware and software systems. Its use has however been limited to control-dominated applications because of a lack of algorithms for computing interpolants for data structures used in software programs. We present efficient procedures to construct interpolants for the theories of arrays, sets, and multisets using the reduction approach for obtaining decision procedures for complex data structures. The approach taken is that of reducing the theories of such data structures to the theories of equality and linear arithmetic for which efficient interpolating decision procedures exist. This enables interpolation based techniques to be applied to proving properties of programs that manipulate these data structures.