D
2018
Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?
JONÁŠ, Martin a Jan STREJČEK
Základní údaje
Originální název
Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?
Vydání
Neuveden, LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, od s. 488-497, 10 s. 2018
Další údaje
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Velká Británie a Severní Irsko
Utajení
není předmětem státního či obchodního tajemství
Forma vydání
elektronická verze "online"
Kód RIV
RIV/00216224:14330/18:00101333
Organizační jednotka
Fakulta informatiky
Klíčová slova anglicky
satisfiability modulo theories; quantified bit-vectors; bit-width; experimental evaluation
Příznaky
Mezinárodní význam, Recenzováno
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.
Návaznosti
GBP202/12/G061, projekt VaV | Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI) | Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky |
|
MUNI/A/0854/2017, interní kód MU | Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII. | Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty |
|
MUNI/A/1038/2017, interní kód MU | Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18 | Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty |
|
Zobrazeno: 28. 10. 2024 16:12