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

D 2018

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

JONÁŠ, Martin and Jan STREJČEK

Basic information

Original name

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

Authors

JONÁŠ, Martin (203 Czech Republic, belonging to the institution) and Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution)

Edition

Neuveden, LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, p. 488-497, 10 pp. 2018

Publisher

EasyChair

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United Kingdom of Great Britain and Northern Ireland

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

electronic version available online

References:

URL

RIV identification code

RIV/00216224:14330/18:00101333

Organization unit

Faculty of Informatics

ISSN

DOI

http://dx.doi.org/10.29007/spnx

Keywords in English

satisfiability modulo theories; quantified bit-vectors; bit-width; experimental evaluation

Abstract

V originále

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.

Links

GBP202/12/G061, research and development project

Name: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Acronym: CE-ITI)

Investor: Czech Science Foundation

MUNI/A/0854/2017, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII.

Investor: Masaryk University, Category A

MUNI/A/1038/2017, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18

Investor: Masaryk University, Category A

Citovat

JONÁŠ, Martin and Jan STREJČEK. Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?. Online. In Gilles Barthe, Geoff Sutcliffe, Margus Veanes. LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Neuveden: EasyChair, 2018, p. 488-497. ISSN 2398-7340. Available from: https://dx.doi.org/10.29007/spnx.

@inproceedings{1464757,
   author = {Jonáš, Martin and Strejček, Jan},
   address = {Neuveden},
   booktitle = {LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
   doi = {http://dx.doi.org/10.29007/spnx},
   editor = {Gilles Barthe, Geoff Sutcliffe, Margus Veanes},
   keywords = {satisfiability modulo theories; quantified bit-vectors; bit-width; experimental evaluation},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Neuveden},
   pages = {488-497},
   publisher = {EasyChair},
   title = {Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?},
   url = {https://easychair.org/publications/paper/wPNs},
   year = {2018}
}

TY  - JOUR
ID  - 1464757
AU  - Jonáš, Martin - Strejček, Jan
PY  - 2018
TI  - Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?
PB  - EasyChair
CY  - Neuveden
KW  - satisfiability modulo theories
KW  - quantified bit-vectors
KW  - bit-width
KW  - experimental evaluation
UR  - https://easychair.org/publications/paper/wPNs
N2  - 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.
ER  -

JONÁŠ, Martin and Jan STREJČEK. Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?. Online. In Gilles Barthe, Geoff Sutcliffe, Margus Veanes. \textit{LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning}. Neuveden: EasyChair, 2018, p.~488-497. ISSN~2398-7340. Available from: https://dx.doi.org/10.29007/spnx.

Detailed Information on Publication Record