uu.seUppsala universitets publikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
An approximation framework for solvers and decision procedures
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. (Embedded Systems)
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. (Embedded Systems)ORCID-id: 0000-0002-2733-7098
2017 (Engelska)Ingår i: Journal of automated reasoning, ISSN 0168-7433, E-ISSN 1573-0670, Vol. 58, nr 1, s. 127-147Artikel i tidskrift (Refereegranskat) Published
Ort, förlag, år, upplaga, sidor
2017. Vol. 58, nr 1, s. 127-147
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
URN: urn:nbn:se:uu:diva-305180DOI: 10.1007/s10817-016-9393-1ISI: 000392387400006OAI: oai:DiVA.org:uu-305180DiVA, id: diva2:1034538
Projekt
UPMARCTillgänglig från: 2016-11-10 Skapad: 2016-10-12 Senast uppdaterad: 2018-01-14Bibliografiskt granskad
Ingår i avhandling
1. Approximations and abstractions for reasoning about machine arithmetic
Öppna denna publikation i ny flik eller fönster >>Approximations and abstractions for reasoning about machine arithmetic
2016 (Engelska)Licentiatavhandling, sammanläggning (Övrigt vetenskapligt)
Abstract [en]

Safety-critical systems rely on various forms of machine arithmetic to perform their tasks: integer arithmetic, fixed-point arithmetic or floating-point arithmetic. The problem with machine arithmetic is that it can exhibit subtle differences in behavior compared to the ideal mathematical arithmetic, due to fixed-size representation in memory. Failure of safety-critical systems is unacceptable, because it can cost lives or huge amounts of money, time and effort. To prevent such incidents, we want to formally prove that systems satisfy certain safety properties, or otherwise discover cases when the properties are violated. However, for this we need to be able to formally reason about machine arithmetic. The main problem with existing approaches is their inability to scale well with the increasing complexity of systems and their properties. In this thesis, we explore two alternatives to bit-blasting, the core procedure lying behind many common approaches to reasoning about machine arithmetic.

In the first approach, we present a general approximation framework which we apply to solve constraints over floating-point arithmetic. It is built on top of an existing decision procedure, e.g., bit-blasting. Rather than solving the original formula, we solve a sequence of approximations of the formula. Initially very crude, these approximations are frequently solved very quickly. We use results from these approximations to either obtain a solution, obtain a proof of unsatisfiability or generate a new approximation to solve. Eventually, we will either have found a solution or a proof that solution does not exist. The approximation framework improves the solving time and can solve a number of formulas that the bit-blasting cannot.

In the second approach, we present a novel method to reason about the theory of fixed-width bit-vectors. This new decision procedure is called mcBV and it is based on the model constructing satisfiability calculus (mcSAT). The procedure uses a lazy representation of bit-vectors and attempts to avoid bit-blasting altogether. It is able to reason about bit-vectors on both bit- and word-level, leveraging both Boolean constraint propagation and native arithmetic reasoning. It also features a greedy explanation generalization mechanism and is capable of more general learning compared to existing approaches. mcBV is able to reason about bit-vectors with sizes that significantly exceed the usual 32, 64 and 128 bits. Evaluation of mcBV shows an improvement in performance (compared to bit-blasting) on several classes of problems.

Ort, förlag, år, upplaga, sidor
Uppsala University, 2016
Serie
IT licentiate theses / Uppsala University, Department of Information Technology, ISSN 1404-5117 ; 2016-010
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
Datavetenskap med inriktning mot inbyggda system
Identifikatorer
urn:nbn:se:uu:diva-305190 (URN)
Handledare
Projekt
UPMARC
Tillgänglig från: 2016-10-12 Skapad: 2016-10-12 Senast uppdaterad: 2019-02-25Bibliografiskt granskad
2. From Machine Arithmetic to Approximations and back again: Improved SMT Methods for Numeric Data Types
Öppna denna publikation i ny flik eller fönster >>From Machine Arithmetic to Approximations and back again: Improved SMT Methods for Numeric Data Types
2017 (Engelska)Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
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.

Ort, förlag, år, upplaga, sidor
Uppsala: Acta Universitatis Upsaliensis, 2017. s. 55
Serie
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1603
Nyckelord
SMT, Model construction, Approximations, floating-point arithmetic, machine arithmetic, bit-vectors
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
Datavetenskap
Identifikatorer
urn:nbn:se:uu:diva-334565 (URN)978-91-513-0162-4 (ISBN)
Disputation
2018-01-23, ITC/2446, Lägerhyddsvägen 2, Uppsala, 09:00 (Engelska)
Opponent
Handledare
Tillgänglig från: 2017-12-19 Skapad: 2017-11-24 Senast uppdaterad: 2018-03-08

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltext

Personposter BETA

Zeljic, AleksandarRümmer, Philipp

Sök vidare i DiVA

Av författaren/redaktören
Zeljic, AleksandarRümmer, Philipp
Av organisationen
Datorteknik
I samma tidskrift
Journal of automated reasoning
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 662 träffar
RefereraExporteraLänk till posten
Permanent länk

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