uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Approximations for Model Construction
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Embedded Systems)
Microsoft Research Cambridge.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Embedded Systems)
2014 (English)In: Automated Reasoning, Springer, 2014, 344-359 p.Conference paper, Published paper (Refereed)
Abstract [en]

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.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8562
Keyword [en]
theorem proving, model construction, first-order logic, floating-point arithmetic
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-238017DOI: 10.1007/978-3-319-08587-6_26ISI: 000345093000027ISBN: 978-3-319-08586-9 (print)ISBN: 978-3-319-08587-6 (print)OAI: oai:DiVA.org:uu-238017DiVA: diva2:769805
Conference
7th International Joint Conference on Automated Reasoning (IJCAR 2014) Held as Part of theVienna Summer of Logic (VSL), 19-22 July 2014, Vienna, Austria
Projects
UPMARC
Available from: 2014-12-09 Created: 2014-12-09 Last updated: 2017-12-01Bibliographically approved

Open Access in DiVA

fulltext(423 kB)44 downloads
File information
File name FULLTEXT01.pdfFile size 423 kBChecksum SHA-512
263812123a32e8ac92562e2ba1e426f4f96e82f4537441746565d6895daf8d8a37f0565907fcd3e6960f7949108f7598210b8b0218ba368a3c2fe66e87ae968c
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Authority records BETA

Zeljic, AleksandarRümmer, Philipp

Search in DiVA

By author/editor
Zeljic, AleksandarRümmer, Philipp
By organisation
Computer Systems
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 44 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 372 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf