uu.seUppsala University Publications

Please wait ... |

Link to record
http://uu.diva-portal.org/smash/person.jsf?pid=authority-person:20389 $(function(){PrimeFaces.cw("InputTextarea","widget_formSmash_upper_j_idt122_recordDirectLink",{id:"formSmash:upper:j_idt122:recordDirectLink",widgetVar:"widget_formSmash_upper_j_idt122_recordDirectLink",autoResize:true});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_upper_j_idt122_j_idt124",{id:"formSmash:upper:j_idt122:j_idt124",widgetVar:"widget_formSmash_upper_j_idt122_j_idt124",target:"formSmash:upper:j_idt122:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});

Permanent link

Direct link

Zeljic, Aleksandar

Open this publication in new window or tab >>Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction### Backeman, Peter

### Rümmer, Philipp

### Zeljic, Aleksandar

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_0_j_idt188_some",{id:"formSmash:j_idt184:0:j_idt188:some",widgetVar:"widget_formSmash_j_idt184_0_j_idt188_some",multiple:true}); PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_0_j_idt188_otherAuthors",{id:"formSmash:j_idt184:0:j_idt188:otherAuthors",widgetVar:"widget_formSmash_j_idt184_0_j_idt188_otherAuthors",multiple:true}); 2018 (English)In: Formal Methods in Computer-Aided Design / [ed] Nikolaj Bjørner, Arie Gurfinkel, IEEE, 2018, p. 50-59Conference paper, Published paper (Refereed)
##### Abstract [en]

##### Place, publisher, year, edition, pages

IEEE, 2018
##### National Category

Computer Sciences
##### Identifiers

urn:nbn:se:uu:diva-368030 (URN)10.23919/FMCAD.2018.8603023 (DOI)000493916300012 ()978-0-9835678-8-2 (ISBN)
##### Conference

The eighteenth in a series of conferences on the theory and applications of formal methods in hardware and system verification (FMCAD 2018), 30 October - 2 November, 2018, University of Texas, Austin, Texas.
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_0_j_idt188_j_idt359",{id:"formSmash:j_idt184:0:j_idt188:j_idt359",widgetVar:"widget_formSmash_j_idt184_0_j_idt188_j_idt359",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_0_j_idt188_j_idt365",{id:"formSmash:j_idt184:0:j_idt188:j_idt365",widgetVar:"widget_formSmash_j_idt184_0_j_idt188_j_idt365",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_0_j_idt188_j_idt371",{id:"formSmash:j_idt184:0:j_idt188:j_idt371",widgetVar:"widget_formSmash_j_idt184_0_j_idt188_j_idt371",multiple:true});
#####

##### Funder

Swedish Research Council, 2014-5484Swedish Foundation for Strategic Research , RIT17-0011
Available from: 2018-12-04 Created: 2018-12-04 Last updated: 2019-12-06Bibliographically approved

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.

The inference of program invariants over machine arithmetic, commonly called bit-vector arithmetic, is an important problem in verification. Techniques that have been successful for unbounded arithmetic, in particular Craig interpolation, have turned out to be difficult to generalise to machine arithmetic: existing bit-vector interpolation approaches are based either on eager translation from bit-vectors to unbounded arithmetic, resulting in complicated constraints that are hard to solve and interpolate, or on bit-blasting to propositional logic, in the process losing all arithmetic structure. We present a new approach to bitvector interpolation, as well as bit-vector quantifier elimination (QE), that works by lazy translation of bit-vector constraints to unbounded arithmetic. Laziness enables us to fully utilise the information available during proof search (implied by decisions and propagation) in the encoding, and this way produce constraints that can be handled relatively easily by existing interpolation and QE procedures for Presburger arithmetic. The lazy encoding is complemented with a set of native proof rules for bit-vector equations and non-linear (polynomial) constraints, this way minimising the number of cases a solver has to consider

Open this publication in new window or tab >>Exploring Approximations for Floating-Point Arithmetic using UppSAT### Zeljic, Aleksandar

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.### Backeman, Peter

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.### Wintersteiger, Christoph M.

### Rümmer, Philipp

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_1_j_idt188_some",{id:"formSmash:j_idt184:1:j_idt188:some",widgetVar:"widget_formSmash_j_idt184_1_j_idt188_some",multiple:true}); PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_1_j_idt188_otherAuthors",{id:"formSmash:j_idt184:1:j_idt188:otherAuthors",widgetVar:"widget_formSmash_j_idt184_1_j_idt188_otherAuthors",multiple:true}); 2018 (English)In: Automated Reasoning / [ed] Didier Galmiche, Stephan Schulz, Roberto Sebastiani, Springer, 2018, p. 246-262Conference paper, Published paper (Refereed)
##### Abstract [en]

##### Place, publisher, year, edition, pages

Springer, 2018
##### Series

Lecture Notes in Computer Science, ISSN 0302-9743 ; 10900
##### National Category

Computer Sciences
##### Research subject

Computer Science
##### Identifiers

urn:nbn:se:uu:diva-368468 (URN)10.1007/978-3-319-94205-6_17 (DOI)000470004600017 ()978-3-319-94204-9 (ISBN)978-3-319-94205-6 (ISBN)
##### Conference

9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_1_j_idt188_j_idt359",{id:"formSmash:j_idt184:1:j_idt188:j_idt359",widgetVar:"widget_formSmash_j_idt184_1_j_idt188_j_idt359",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_1_j_idt188_j_idt365",{id:"formSmash:j_idt184:1:j_idt188:j_idt365",widgetVar:"widget_formSmash_j_idt184_1_j_idt188_j_idt365",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_1_j_idt188_j_idt371",{id:"formSmash:j_idt184:1:j_idt188:j_idt371",widgetVar:"widget_formSmash_j_idt184_1_j_idt188_j_idt371",multiple:true});
#####

##### Funder

Swedish Research Council, 2014-5484
Available from: 2018-12-04 Created: 2018-12-04 Last updated: 2019-06-26Bibliographically approved

Microsoft Research, Cambridge, UK.

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.

Open this publication in new window or tab >>An approximation framework for solvers and decision procedures### Zeljic, Aleksandar

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.### Wintersteiger, Christoph M.

### Rümmer, Philipp

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_2_j_idt188_some",{id:"formSmash:j_idt184:2:j_idt188:some",widgetVar:"widget_formSmash_j_idt184_2_j_idt188_some",multiple:true}); PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_2_j_idt188_otherAuthors",{id:"formSmash:j_idt184:2:j_idt188:otherAuthors",widgetVar:"widget_formSmash_j_idt184_2_j_idt188_otherAuthors",multiple:true}); 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 ()
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_2_j_idt188_j_idt359",{id:"formSmash:j_idt184:2:j_idt188:j_idt359",widgetVar:"widget_formSmash_j_idt184_2_j_idt188_j_idt359",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_2_j_idt188_j_idt365",{id:"formSmash:j_idt184:2:j_idt188:j_idt365",widgetVar:"widget_formSmash_j_idt184_2_j_idt188_j_idt365",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_2_j_idt188_j_idt371",{id:"formSmash:j_idt184:2:j_idt188:j_idt371",widgetVar:"widget_formSmash_j_idt184_2_j_idt188_j_idt371",multiple:true});
#####

##### Projects

UPMARC
Available from: 2016-11-10 Created: 2016-10-12 Last updated: 2018-01-14Bibliographically approved

Open this publication in new window or tab >>Deciding bit-vector formulas with mcSAT### Zeljic, Aleksandar

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.### Wintersteiger, Christoph M.

### Rümmer, Philipp

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_3_j_idt188_some",{id:"formSmash:j_idt184:3:j_idt188:some",widgetVar:"widget_formSmash_j_idt184_3_j_idt188_some",multiple:true}); PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_3_j_idt188_otherAuthors",{id:"formSmash:j_idt184:3:j_idt188:otherAuthors",widgetVar:"widget_formSmash_j_idt184_3_j_idt188_otherAuthors",multiple:true}); 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
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_3_j_idt188_j_idt359",{id:"formSmash:j_idt184:3:j_idt188:j_idt359",widgetVar:"widget_formSmash_j_idt184_3_j_idt188_j_idt359",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_3_j_idt188_j_idt365",{id:"formSmash:j_idt184:3:j_idt188:j_idt365",widgetVar:"widget_formSmash_j_idt184_3_j_idt188_j_idt365",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_3_j_idt188_j_idt371",{id:"formSmash:j_idt184:3:j_idt188:j_idt371",widgetVar:"widget_formSmash_j_idt184_3_j_idt188_j_idt371",multiple:true});
#####

##### Projects

UPMARC
Available from: 2016-06-11 Created: 2016-10-12 Last updated: 2018-01-14Bibliographically approved

Open this publication in new window or tab >>Approximations for Model Construction### Zeljic, Aleksandar

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.### Wintersteiger, Christoph M.

### Rümmer, Philipp

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_4_j_idt188_some",{id:"formSmash:j_idt184:4:j_idt188:some",widgetVar:"widget_formSmash_j_idt184_4_j_idt188_some",multiple:true}); PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_4_j_idt188_otherAuthors",{id:"formSmash:j_idt184:4:j_idt188:otherAuthors",widgetVar:"widget_formSmash_j_idt184_4_j_idt188_otherAuthors",multiple:true}); 2014 (English)In: Automated Reasoning, Springer, 2014, p. 344-359Conference paper, Published paper (Refereed)
##### Abstract [en]

##### Place, publisher, year, edition, pages

Springer, 2014
##### Series

Lecture Notes in Computer Science, ISSN 0302-9743 ; 8562
##### Keywords

theorem proving, model construction, first-order logic, floating-point arithmetic
##### National Category

Computer Sciences
##### Identifiers

urn:nbn:se:uu:diva-238017 (URN)10.1007/978-3-319-08587-6_26 (DOI)000345093000027 ()978-3-319-08586-9 (ISBN)978-3-319-08587-6 (ISBN)
##### 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
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_4_j_idt188_j_idt359",{id:"formSmash:j_idt184:4:j_idt188:j_idt359",widgetVar:"widget_formSmash_j_idt184_4_j_idt188_j_idt359",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_4_j_idt188_j_idt365",{id:"formSmash:j_idt184:4:j_idt188:j_idt365",widgetVar:"widget_formSmash_j_idt184_4_j_idt188_j_idt365",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt184_4_j_idt188_j_idt371",{id:"formSmash:j_idt184:4:j_idt188:j_idt371",widgetVar:"widget_formSmash_j_idt184_4_j_idt188_j_idt371",multiple:true});
#####

##### Projects

UPMARC
Available from: 2014-12-09 Created: 2014-12-09 Last updated: 2018-01-11Bibliographically approved

Microsoft Research Cambridge.

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.