Caricamento...

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

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,...

Descrizione completa

Salvato in:
Dettagli Bibliografici
Pubblicato in:Tools and Algorithms for the Construction and Analysis of Systems
Autori principali: Okudono, Takamasa, King, Andy
Natura: Artigo
Lingua:Inglês
Pubblicazione: 2020
Soggetti:
Accesso online:https://ncbi.nlm.nih.gov/pmc/articles/PMC7439747/
https://ncbi.nlm.nih.govhttp://dx.doi.org/10.1007/978-3-030-45190-5_5
Tags: Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne! !