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

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

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

An Entity of Type : schema:ScholarlyArticle, within Data Space : wasabi.inria.fr associated with source document(s)

Attributes	Values
type	Academic Article research paper schema:ScholarlyArticle
isDefinedBy	Covid-on-the-Web dataset
title	Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
Creator	King, Andy Okudono, Takamasa
source	PMC
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.
has issue date	2020-03-13(xsd:dateTime)
bibo:doi	10.1007/978-3-030-45190-5_5
has license	cc-by
sha1sum (hex)	d4b50ef79735dfe99adea35bf7fa89ea18703a3e
schema:url	https://doi.org/10.1007/978-3-030-45190-5_5
resource representing a document's title	Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
has PubMed Central identifier	PMC7439747
schema:publication	Tools and Algorithms for the Construction and Analysis of Systems
resource representing a document's body	covid:d4b50ef79735dfe99adea35bf7fa89ea18703a3e#body_text
is schema:about of	named entity 'LIA' named entity 'gapping' named entity 'modeled' named entity 'TRANSLATING' named entity 'DEMONSTRATED' named entity 'COMPLETED BY' named entity 'time' named entity 'translated' named entity 'interpolant' named entity 'completed' named entity 'process' named entity 'LIA' named entity 'This' named entity 'interpolation' named entity 'arithmetic' named entity 'interpolant' named entity 'interpolant' named entity 'parses' named entity 'interpolant' named entity 'syntactic' named entity 'semantics' named entity 'polynomial' named entity 'model checker' named entity 'C language' named entity 'semantics' named entity 'model checker' named entity 'integer arithmetic' named entity 'intuition' named entity 'interpolant' named entity 'interpolant' named entity 'propositional formulae' named entity 'interpolant' named entity 'interpolant' named entity 'interpolant' named entity 'logical connectives' named entity 'arithmetic' named entity 'execution times' named entity '1, 2' named entity 'interpolant' named entity 'theorem provers' named entity 'Abstract domains' named entity 'fixpoint' named entity 'linear congruence' named entity 'semantics' named entity 'semantics' named entity 'monotonically' named entity 'intuition' named entity 'subset' named entity 'logical connectives' named entity 'propositionally' named entity 'interpolant' named entity 'interpolant' named entity 'model-checker' named entity 'interpolant' named entity 'positive integers' named entity 'disjuncts' named entity 'mixed integer' named entity 'scatter plot' named entity 'interpolant' named entity '2, 3' named entity 'algorithm' named entity 'integer overflow' named entity 'scatter plot' named entity 'linear inequalities' named entity 'predicates' named entity 'program state' named entity 'model checking' named entity 'arithmetic' named entity 'model checking' named entity 'non-negative integer' named entity 'arithmetic' named entity 'logic' named entity 'arithmetic' named entity 'arithmetic' named entity '7.5' named entity 'interpolant' named entity 'interpolant' named entity 'finite set' named entity 'real numbers' named entity 'scatter plot' named entity 'arithmetic' named entity 'semantics'

Faceted Search & Find service v1.13.91 as of Mar 24 2020

Alternative Linked Data Documents: Sponger | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2025 OpenLink Software