Approximations for Model Construction

Aleksandar Zeljic, Uppsala University

Wednesday, December 10th, 2014 at 15:15.

Polacksbacken, room 1245

We consider the problem of efficiently computing models for
satisfiable constraints, in the presence of complex background
theories such as floating-point arithmetic. Model construction
has various applications, for instance the automatic generation of
test inputs. It is well-known that naive encoding of constraints
into simpler theories (for instance, bit-vectors or propositional
logic) can lead to a drastic increase in size, and be unsatisfactory
in terms of memory and runtime needed for model construction. We
define a framework for systematic application of approximations in
order to speed up model construction. Our method is more general
than previous techniques in the sense that approximations that
are neither under- nor over-approximations can be used, and
shows promising results in practice.

Joint work with Philipp Ruemmer and Christoph M. Wintersteiger.