Aleksandar Zeljic, Christoph M. Wintersteiger, and Philipp Rummer
We consider the problem of efficiently computing models for satisfiable constraints, in the presence of complex background theories such as oating-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.
|Published in||Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR 2014)|
IJCAR 2014 best paper award! http://vsl2014.at/2014/07/ijcar-best-paper-award/