Approximations for Model Construction
2014 (English)In: Automated Reasoning, Springer, 2014, 344-359 p.Conference paper (Refereed)
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.
Place, publisher, year, edition, pages
Springer, 2014. 344-359 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 8562
theorem proving, model construction, first-order logic, floating-point arithmetic
IdentifiersURN: urn:nbn:se:uu:diva-238017DOI: 10.1007/978-3-319-08587-6_26ISI: 000345093000027ISBN: 978-3-319-08586-9ISBN: 978-3-319-08587-6OAI: oai:DiVA.org:uu-238017DiVA: diva2:769805
7th International Joint Conference on Automated Reasoning (IJCAR 2014) Held as Part of theVienna Summer of Logic (VSL), 19-22 July 2014, Vienna, Austria