Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • 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
From Machine Arithmetic to Approximations and back again: Improved SMT Methods for Numeric Data Types
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
2017 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Safety-critical systems, especially those found in avionics and automotive industries, rely on machine arithmetic to perform their tasks: integer arithmetic, fixed-point arithmetic or floating-point arithmetic (FPA). Machine arithmetic exhibits subtle differences in behavior compared to the ideal mathematical arithmetic, due to fixed-size representation in memory. Failure of safety-critical systems is unacceptable, due to high-stakes involving human lives or huge amounts of money, time and effort. By formally proving properties of systems, we can be assured that they meet safety requirements. However, to prove such properties it is necessary to reason about machine arithmetic. SMT techniques for machine arithmetic are lacking scalability. This thesis presents approaches that augment or complement existing SMT techniques for machine arithmetic.

In this thesis, we explore approximations as a means of augmenting existing decision procedures. A general approximation refinement framework is presented, along with its implementation called UppSAT. The framework solves a sequence of approximations. Initially very crude, these approximations are fairly easy to solve. Results of solving approximate constraints are used to either reconstruct a solution of original constraints, obtain a proof of unsatisfiability or to refine the approximation. The framework preserves soundness, completeness, and termination of the underlying decision procedure, guaranteeing that eventually, either a solution is found or a proof that solution does not exist. We evaluate the impact of approximations implemented in the UppSAT framework on the state-of-the-art in SMT for floating-point arithmetic.

A novel method to reason about the theory of fixed-width bit-vectors called mcBV is presented. It is an instantiation of the model constructing satisfiability calculus, mcSAT, and uses a new lazy representation of bit-vectors that allows both bit- and word-level reasoning. It uses a greedy explanation generalization mechanism capable of more general learning compared to traditional approaches. Evaluation of mcBV shows that it can outperform bit-blasting on several classes of problems.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2017. , p. 55
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1603
Keywords [en]
SMT, Model construction, Approximations, floating-point arithmetic, machine arithmetic, bit-vectors
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-334565ISBN: 978-91-513-0162-4 (print)OAI: oai:DiVA.org:uu-334565DiVA, id: diva2:1159882
Public defence
2018-01-23, ITC/2446, Lägerhyddsvägen 2, Uppsala, 09:00 (English)
Opponent
Supervisors
Available from: 2017-12-19 Created: 2017-11-24 Last updated: 2018-03-08
List of papers
1. Deciding bit-vector formulas with mcSAT
Open this publication in new window or tab >>Deciding bit-vector formulas with mcSAT
2016 (English)In: Theory and Applications of Satisfiability Testing: SAT 2016, Springer, 2016, p. 249-266Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer, 2016
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9710
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-305182 (URN)10.1007/978-3-319-40970-2_16 (DOI)000387430600016 ()978-3-319-40969-6 (ISBN)
Conference
SAT 2016, July 5–8, Bordeaux, France
Projects
UPMARC
Available from: 2016-06-11 Created: 2016-10-12 Last updated: 2018-01-14Bibliographically approved
2. An approximation framework for solvers and decision procedures
Open this publication in new window or tab >>An approximation framework for solvers and decision procedures
2017 (English)In: Journal of automated reasoning, ISSN 0168-7433, E-ISSN 1573-0670, Vol. 58, no 1, p. 127-147Article in journal (Refereed) Published
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-305180 (URN)10.1007/s10817-016-9393-1 (DOI)000392387400006 ()
Projects
UPMARC
Available from: 2016-11-10 Created: 2016-10-12 Last updated: 2018-01-14Bibliographically approved
3. Exploring Approximations for Floating-Point Arithmetic using UppSAT
Open this publication in new window or tab >>Exploring Approximations for Floating-Point Arithmetic using UppSAT
(English)Manuscript (preprint) (Other academic)
Abstract [en]

We consider the problem of solving floating-point constraints obtained from software verification. We present UppSAT --- a new implementation of a systematic approximation refinement framework [ZWR17] 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 several approximations of floating-point arithmetic. Approximations can be viewed as a composition of an encoding into a target theory, a precision ordering, and a number of strategies for model reconstruction and precision (or approximation) refinement. We present 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 (based on existing, state-of-the-art SMT solvers for floating-point, real, and bit-vector arithmetic).

Keywords
SAT, SMT, approximations, model construction, floating-point arithmetic
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-334564 (URN)
Available from: 2017-11-24 Created: 2017-11-24 Last updated: 2018-01-13

Open Access in DiVA

fulltext(491 kB)101 downloads
File information
File name FULLTEXT01.pdfFile size 491 kBChecksum SHA-512
dc91be8e3e48293a5292c753889f3bc6485d3db11b524d8a50fdfdacbe3971a553a49cdd6e41b4c01216f5a5090dde98089d18c762d7e94af623d75674ded973
Type fulltextMimetype application/pdf
Buy this publication >>

By organisation
Division of Computer SystemsComputing Science
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 101 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

isbn
urn-nbn

Altmetric score

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

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • 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