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?

Autoři

JONÁŠ, Martin (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí)

Vydání

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

Nakladatel

EasyChair

Další údaje

Jazyk

angličtina

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"

Odkazy

URL

Kód RIV

RIV/00216224:14330/18:00101333

Organizační jednotka

Fakulta informatiky

ISSN

DOI

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

Klíčová slova anglicky

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

Štítky

core_A, firank_A, formela-conference

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 31. 5. 2022 14:22, RNDr. Pavel Šmerk, Ph.D.

Anotace

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