https://www.mdu.se/

mdu.sePublications
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
Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
Uppsala Univ, Dept Informat Technol, Uppsala, Sweden..
Stanford Univ, Stanford, CA 94305 USA..
2021 (English)In: Formal methods in system design, ISSN 0925-9856, E-ISSN 1572-8102, Vol. 57, no 2, p. 121-156Article in journal (Refereed) Published
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 bit-vector 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. We also incorporate a method for handling concatenations and extractions of bit-vector efficiently.

Place, publisher, year, edition, pages
SPRINGER , 2021. Vol. 57, no 2, p. 121-156
Keywords [en]
Bit-vectors, Interpolation, Quantifier elimination, Presburger arithmetic
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-54409DOI: 10.1007/s10703-021-00372-6ISI: 000650085300001Scopus ID: 2-s2.0-85105874949OAI: oai:DiVA.org:mdh-54409DiVA, id: diva2:1559881
Available from: 2021-06-03 Created: 2021-06-03 Last updated: 2021-12-16Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Backeman, Peter

Search in DiVA

By author/editor
Backeman, Peter
By organisation
Embedded Systems
In the same journal
Formal methods in system design
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 63 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