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

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

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

<a href="/cs/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Centrum excelence - Institut teoretické informatiky (CE-ITI)</a><br>

Návaznosti

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

Rok uplatnění

2018

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

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

ISBN

—

ISSN

2398-7340

e-ISSN

—

Počet stran výsledku

10

Strana od-do

488-497

Název nakladatele

EasyChair

Místo vydání

Neuveden

Místo konání akce

Awassa, Ethiopia

Datum konání akce

1. 1. 2018

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

WRD - Celosvětová akce

Kód UT WoS článku

—