Skip to main content

Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic

Okudono, Takamasa and King, Andy (2020) Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic. In: Biere, Armin and Parker, David, eds. International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, pp. 79-96. ISBN 978-3-030-45189-9. (doi:10.1007/978-3-030-45190-5_5) (KAR id:80188)

PDF Publisher pdf
Language: English


Creative Commons Licence
This work is licensed under a Creative Commons Attribution 4.0 International License.
Download (652kB) Preview
[img]
Preview
Official URL
https://doi.org/10.1007/978-3-030-45190-5_5

Abstract

Much of an interpolation engine for bit-vector (BV) arithmetic can be constructed by observing that BV arithmetic can be modeled with linear integer arithmetic (LIA). Two BV formulae can thus be translated into two LIA formulae and then an interpolation engine for LIA used to derive an interpolant, albeit one expressed in LIA. The construction is completed by back-translating the LIA interpolant into a BV formula whose models coincide with those of the LIA interpolant. This paper develops a back-translation algorithm showing, for the first time, how back-translation can be universally applied, whatever the LIA interpolant. This avoids the need for deriving a BV interpolant by bit-blasting the BV formulae, as a backup process when back-translation fails. The new back-translation process relies on a novel geometric technique, called gapping, the correctness and practicality of which are demonstrated.

Item Type: Book section
DOI/Identification number: 10.1007/978-3-030-45190-5_5
Uncontrolled keywords: BV arithmetic, LIA
Subjects: Q Science > QA Mathematics (inc Computing science)
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Andy King
Date Deposited: 21 Feb 2020 14:30 UTC
Last Modified: 16 Jun 2020 12:21 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/80188 (The current URI for this page, for reference purposes)
King, Andy: https://orcid.org/0000-0001-5806-4822
  • Depositors only (login required):

Downloads

Downloads per month over past year