Fast Three-Valued Abstract Bit-Vector Arithmetic

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F22%3A00556720" target="_blank" >RIV/67985807:_____/22:00556720 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/68407700:21240/22:00354870

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-030-94583-1_12" target="_blank" >http://dx.doi.org/10.1007/978-3-030-94583-1_12</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-94583-1_12" target="_blank" >10.1007/978-3-030-94583-1_12</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Fast Three-Valued Abstract Bit-Vector Arithmetic

Popis výsledku v původním jazyce

Abstraction is one of the most important approaches for reducing the number of states in formal verification. An important abstraction technique is the usage of three-valued logic, extensible to bit-vectors. The best abstract bit-vector results for movement and logical operations can be computed quickly. However, for widely-used arithmetic operations, efficient algorithms for computation of the best possible output have not been known up to now. In this paper, we present new efficient polynomial-time algorithms for abstract addition and multiplication with three-valued bit-vector inputs. These algorithms produce the best possible three-valued bit-vector output and remain fast even with 32-bit inputs. To obtain the algorithms, we devise a novel modular extreme-finding technique via reformulation of the problem using pseudo-Boolean modular inequalities. Using the introduced technique, we construct an algorithm for abstract addition that computes its result in linear time, as well as a worst-case quadratic-time algorithm for abstract multiplication. Finally, we experimentally evaluate the performance of the algorithms, confirming their practical efficiency.

Název v anglickém jazyce

Fast Three-Valued Abstract Bit-Vector Arithmetic

Popis výsledku anglicky

Abstraction is one of the most important approaches for reducing the number of states in formal verification. An important abstraction technique is the usage of three-valued logic, extensible to bit-vectors. The best abstract bit-vector results for movement and logical operations can be computed quickly. However, for widely-used arithmetic operations, efficient algorithms for computation of the best possible output have not been known up to now. In this paper, we present new efficient polynomial-time algorithms for abstract addition and multiplication with three-valued bit-vector inputs. These algorithms produce the best possible three-valued bit-vector output and remain fast even with 32-bit inputs. To obtain the algorithms, we devise a novel modular extreme-finding technique via reformulation of the problem using pseudo-Boolean modular inequalities. Using the introduced technique, we construct an algorithm for abstract addition that computes its result in linear time, as well as a worst-case quadratic-time algorithm for abstract multiplication. Finally, we experimentally evaluate the performance of the algorithms, confirming their practical efficiency.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2022

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Verification, Model Checking, and Abstract Interpretation

ISBN

978-3-030-94582-4

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

21

Strana od-do

242-262

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Philadelphia

Datum konání akce

16. 1. 2022

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

001059208500012