Další formáty:
BibTeX
LaTeX
RIS
@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 a 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, s.~488-497. ISSN~2398-7340. Dostupné z: https://dx.doi.org/10.29007/spnx.
|