Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F18%3A00101333" target="_blank" >RIV/00216224:14330/18:00101333 - isvavai.cz</a>

Result on the web

<a href="http://dx.doi.org/10.29007/spnx" target="_blank" >http://dx.doi.org/10.29007/spnx</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.29007/spnx" target="_blank" >10.29007/spnx</a>

Result language

angličtina

Original language name

Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?

Original language description

In general, deciding satisfiability of quantified bit-vector formulas becomes harder with increasing maximal allowed bit-width of variables and constants. However, this does not have to be the case for formulas that come from practical applications. For example, software bugs often do not depend on the specific bit-width of the program variables and would manifest themselves also with much lower bit-widths. We experimentally evaluate this thesis and show that satisfiability of the vast majority of quantified bit-vector formulas from the smt-lib repository remains the same even after reducing bit-widths of variables to a very small number. This observation may serve as a starting-point for development of heuristics or other techniques that can improve performance of smt solvers for quantified bit-vector formulas.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

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

Project

<a href="/en/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Center of excellence - Institute for theoretical computer science (CE-ITI)</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2018

Confidentiality

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

Article name in the collection

LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning

ISBN

—

ISSN

2398-7340

e-ISSN

—

Number of pages

10

Pages from-to

488-497

Publisher name

EasyChair

Place of publication

Neuveden

Event location

Awassa, Ethiopia

Event date

Jan 1, 2018

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—