This HTML5 document contains 33 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
n6doi:10.1007/
n2https://kar.kent.ac.uk/id/eprint/
n10https://kar.kent.ac.uk/80188/
wdrshttp://www.w3.org/2007/05/powder-s#
dchttp://purl.org/dc/elements/1.1/
n18http://purl.org/ontology/bibo/status/
n13https://kar.kent.ac.uk/id/eprint/80188#
n23https://kar.kent.ac.uk/id/subject/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n15https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/
n3http://eprints.org/ontology/
n16https://kar.kent.ac.uk/id/event/
n11http://www.loc.gov/loc.terms/relators/
bibohttp://purl.org/ontology/bibo/
n17https://kar.kent.ac.uk/id/publication/
n19https://kar.kent.ac.uk/id/org/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
n12https://kar.kent.ac.uk/id/document/
n22https://kar.kent.ac.uk/id/
xsdhhttp://www.w3.org/2001/XMLSchema#
n21https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/
n8https://kar.kent.ac.uk/id/person/

Statements

Subject Item
n2:80188
rdf:type
n3:BookSectionEPrint bibo:Article n3:EPrint bibo:BookSection
rdfs:seeAlso
n10:
owl:sameAs
n6:978-3-030-45190-5_5
n11:EDT
n8:ext-956ad2114e83ab7ad9f61643769038ec n8:ext-686f381942e6526dd6ac9161cd2338dd
n3:hasDocument
n12:3204750 n12:3204751 n12:3204752 n12:3204753 n12:3204754 n12:3204755
n3:hasPublished
n12:3204750
dc:hasVersion
n12:3204750
dcterms:title
Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
wdrs:describedby
n15:export_kar_RDFN3.n3 n21:export_kar_RDFN3.n3
dcterms:date
2020-04-17
dcterms:creator
n8:ext-a.m.king@kent.ac.uk n8:ext-6b4d41da559b321880f6be2fc512a920
bibo:status
n18:peerReviewed n18:published
dcterms:publisher
n19:ext-1c5ddec173ca8cdfba8b274309638579
bibo: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.
dcterms:isPartOf
n17:ext-03029743 n22:repository
dcterms:subject
n23:QA
bibo:authorList
n13:authors
bibo:editorList
n13:editors
bibo:presentedAt
n16:ext-465208b52ab495d6337cf9c287f5fd0c
bibo:volume
12078