“Bit-Precise Reasoning via Int-Blasting” by Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. In Proceedings of the 23^rd International Conference on Verification, Model Checking, and Abstract Interpretion (VMCAI '22), (Bernd Finkbeiner and Thomas Wies, eds.), Jan. 2022, pp. 496-518.
The state of the art for bit-precise reasoning in the context of Satisfiability Modulo Theories (SMT) is a SAT-based technique called bit-blasting where the input formula is first simplified and then translated to an equisatisfiable propositional formula. The main limitation of this technique is scalability, especially in the presence of large bit-widths and arithmetic operators. We introduce an alternative technique, which we call int-blasting, based on a translation to an extension of integer arithmetic rather than propositional logic. We present several translations, discuss their differences, and evaluate them on benchmarks that arise from the verification of rewrite rule candidates for bit-vector solving, as well as benchmarks from SMT-LIB. We also provide preliminary results on 35 benchmarks that arise from smart contract verification. The evaluation shows that this technique is particularly useful for benchmarks with large bit-widths and can solve benchmarks that the state of the art cannot.
BibTeX entry:
@inproceedings{ZIM+22,
author = {Yoni Zohar and Ahmed Irfan and Makai Mann and Aina Niemetz
and Andres N{\"o}tzli and Mathias Preiner and Andrew Reynolds and
Clark Barrett and Cesare Tinelli},
editor = {Bernd Finkbeiner and Thomas Wies},
title = {Bit-Precise Reasoning via Int-Blasting},
booktitle = {Proceedings of the {\it 23^{rd}} International Conference
on Verification, Model Checking, and Abstract Interpretion (VMCAI
'22)},
series = {Lecture Notes in Computer Science},
volume = {13182},
pages = {496--518},
publisher = {Springer},
month = jan,
year = {2022},
doi = {10.1007/978-3-030-94583-1_24},
url = {http://theory.stanford.edu/~barrett/pubs/ZIM+22.pdf}
}
(This webpage was created with bibtex2web.)