uu.seUppsala universitets publikasjoner
Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Exploring Approximations for Floating-Point Arithmetic using UppSAT
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
Microsoft Research, Cambridge, UK.
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. (Embedded Systems)ORCID-id: 0000-0002-2733-7098
2018 (engelsk)Inngår i: Automated Reasoning / [ed] Didier Galmiche, Stephan Schulz, Roberto Sebastiani, Springer, 2018, s. 246-262Konferansepaper, Publicerat paper (Fagfellevurdert)
Abstract [en]

We consider the problem of solving floating-point constraints obtained from software verification. We present UppSAT—an new implementation of a systematic approximation refinement framework as an abstract SMT solver. Provided with an approximation and a decision procedure (implemented in an off-the-shelf SMT solver), UppSAT yields an approximating SMT solver. Additionally, UppSAT includes a library of predefined approximation components which can be combined and extended to define new encodings, orderings and solving strategies. We propose that UppSAT can be used as a sandbox for easy and flexible exploration of new approximations. To substantiate this, we explore encodings of floating-point arithmetic into reduced precision floating-point arithmetic, real-arithmetic, and fixed-point arithmetic (encoded into the theory of bit-vectors in practice). In an experimental evaluation we compare the advantages and disadvantages of approximating solvers obtained by combining various encodings and decision procedures.

sted, utgiver, år, opplag, sider
Springer, 2018. s. 246-262
Serie
Lecture Notes in Computer Science, ISSN 0302-9743 ; 10900
HSV kategori
Forskningsprogram
Datavetenskap
Identifikatorer
URN: urn:nbn:se:uu:diva-368468DOI: 10.1007/978-3-319-94205-6_17ISI: 000470004600017ISBN: 978-3-319-94204-9 (tryckt)ISBN: 978-3-319-94205-6 (digital)OAI: oai:DiVA.org:uu-368468DiVA, id: diva2:1268133
Konferanse
9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018
Forskningsfinansiär
Swedish Research Council, 2014-5484Tilgjengelig fra: 2018-12-04 Laget: 2018-12-04 Sist oppdatert: 2019-06-26bibliografisk kontrollert

Open Access i DiVA

fulltext(510 kB)62 nedlastinger
Filinformasjon
Fil FULLTEXT01.pdfFilstørrelse 510 kBChecksum SHA-512
9321e1e6bb7fbc22dfce1328e8a0e705613e06044b48e17cdc975ac57e1e65f9ec13319d7d65f985408eb89dd952fd84e1e0a549f201728f2f34d1260b923475
Type fulltextMimetype application/pdf

Andre lenker

Forlagets fulltekst

Personposter BETA

Zeljic, AleksandarBackeman, PeterRümmer, Philipp

Søk i DiVA

Av forfatter/redaktør
Zeljic, AleksandarBackeman, PeterRümmer, Philipp
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar
Totalt: 62 nedlastinger
Antall nedlastinger er summen av alle nedlastinger av alle fulltekster. Det kan for eksempel være tidligere versjoner som er ikke lenger tilgjengelige

doi
isbn
urn-nbn

Altmetric

doi
isbn
urn-nbn
Totalt: 80 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf