Department of Information Technology

Approximations for Model Construction


Aleksandar Zeljic, Uppsala University

Date and Time

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.

Updated  2014-12-10 00:03:10 by Jari Stenman.