uu.seUppsala University Publications
Change search
Link to record
Permanent link

Direct link
BETA
Zeljic, Aleksandar
Publications (5 of 5) Show all publications
Backeman, P., Rümmer, P. & Zeljic, A. (2018). Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction. In: Nikolaj Bjørner, Arie Gurfinkel (Ed.), Formal Methods in Computer-Aided Design: . Paper presented at 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. (pp. 50-59). IEEE
Open this publication in new window or tab >>Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction
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]

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

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.
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
Zeljic, A., Backeman, P., Wintersteiger, C. M. & Rümmer, P. (2018). Exploring Approximations for Floating-Point Arithmetic using UppSAT. In: Didier Galmiche, Stephan Schulz, Roberto Sebastiani (Ed.), Automated Reasoning: . Paper presented at 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018 (pp. 246-262). Springer
Open this publication in new window or tab >>Exploring Approximations for Floating-Point Arithmetic using UppSAT
2018 (English)In: Automated Reasoning / [ed] Didier Galmiche, Stephan Schulz, Roberto Sebastiani, Springer, 2018, p. 246-262Conference paper, Published paper (Refereed)
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.

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
Funder
Swedish Research Council, 2014-5484
Available from: 2018-12-04 Created: 2018-12-04 Last updated: 2019-06-26Bibliographically approved
Zeljic, A., Wintersteiger, C. M. & Rümmer, P. (2017). An approximation framework for solvers and decision procedures. Journal of automated reasoning, 58(1), 127-147
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
Zeljic, A., Wintersteiger, C. M. & Rümmer, P. (2016). Deciding bit-vector formulas with mcSAT. In: Theory and Applications of Satisfiability Testing: SAT 2016. Paper presented at SAT 2016, July 5–8, Bordeaux, France (pp. 249-266). Springer
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
Zeljic, A., Wintersteiger, C. M. & Rümmer, P. (2014). Approximations for Model Construction. In: Automated Reasoning: . Paper presented at 7th International Joint Conference on Automated Reasoning (IJCAR 2014) Held as Part of theVienna Summer of Logic (VSL), 19-22 July 2014, Vienna, Austria (pp. 344-359). Springer
Open this publication in new window or tab >>Approximations for Model Construction
2014 (English)In: Automated Reasoning, Springer, 2014, p. 344-359Conference paper, Published paper (Refereed)
Abstract [en]

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.

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
Projects
UPMARC
Available from: 2014-12-09 Created: 2014-12-09 Last updated: 2018-01-11Bibliographically approved
Organisations

Search in DiVA

Show all publications