Sökning: WFRF:(Wintersteiger Christoph M.) >
Exploring Approxima...
Exploring Approximations for Floating-Point Arithmetic using UppSAT
-
- Zeljic, Aleksandar (författare)
- Uppsala universitet,Datorteknik
-
- Backeman, Peter (författare)
- Uppsala universitet,Datorteknik
-
- Wintersteiger, Christoph M. (författare)
- Microsoft Research, Cambridge, UK
-
visa fler...
-
- Rümmer, Philipp, 1978- (författare)
- Uppsala universitet,Datorteknik,Embedded Systems
-
visa färre...
-
(creator_code:org_t)
- 2018-06-30
- 2018
- Engelska.
-
Ingår i: Automated Reasoning. - Cham : Springer International Publishing. - 9783319942049 - 9783319942056 ; , s. 246-262
- Relaterad länk:
-
https://arxiv.org/ab...
-
visa fler...
-
https://uu.diva-port... (primary) (Raw object)
-
http://arxiv.org/pdf...
-
https://urn.kb.se/re...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Computer Science
- Datavetenskap
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)
Hitta via bibliotek
Till lärosätets databas