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

Not logged in : Login

(Sponging disallowed)

Facets (new session)
Description
Metadata
Settings
- Rule:
- Inverse Functional Properties:
- "Same As":

About: Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic Goto Sponge NotDistinct Permalink

An Entity of Type : bibo:BookSection, within Data Space : linkeddata.uriburner.com:28898 associated with source document(s)

Attributes	Values
type	http://eprints.org/ontology/BookSectionEPrint http://eprints.org/ontology/EPrint Article Book Section
seeAlso	HTML Summary of #80188 Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
sameAs	Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
http://www.loc.gov...erms/relators/EDT	Armin Biere David Parker
http://eprints.org/ontology/hasDocument	Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic (PDF) Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic (Other) Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic (Other) Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic (Other) Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic (Other) Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic (Other)
http://eprints.org/ontology/hasPublished	Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic (PDF)
dc:hasVersion	Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic (PDF)
Title	Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
described by	https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/export_kar_RDFN3.n3 https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
Date	2020-04-17
Creator	Takamasa Okudono Andy King
status	peer reviewed published
Publisher	Springer
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.
Is Part Of	Financial Cryptography and Data Security https://kar.kent.ac.uk/id/repository
Subject	QA Mathematics (inc Computing science)
list of authors	https://kar.kent.ac.uk/id/eprint/80188#authors
list of editors	https://kar.kent.ac.uk/id/eprint/80188#editors
presented at	26th International Conference, TACAS 2020
volume	12078
is topic of	https://www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/export_kar_RDFN3.n3 https://raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
is primary topic of	HTML Summary of #80188 Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic

Faceted Search & Find service v1.17_git144 as of Jul 26 2024

Alternative Linked Data Documents: iSPARQL | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 08.03.3331 as of Aug 25 2024, on Linux (x86_64-ubuntu_noble-linux-glibc2.38-64), Single-Server Edition (378 GB total memory, 36 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software