Detailed Information on Publication Record
2018
Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?
JONÁŠ, Martin and Jan STREJČEKBasic 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:
RIV identification code
RIV/00216224:14330/18:00101333
Organization unit
Faculty of Informatics
ISSN
Keywords in English
satisfiability modulo theories; quantified bit-vectors; bit-width; experimental evaluation
Tags
Tags
International impact, Reviewed
Změněno: 31/5/2022 14:22, RNDr. Pavel Šmerk, Ph.D.
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 |
| ||
MUNI/A/0854/2017, interní kód MU |
| ||
MUNI/A/1038/2017, interní kód MU |
|