Bit-Precise Reasoning via Int-BlastingRemote
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 emph{int-blasting}, based on a translation to an extension of integer arithmetic rather than propositional logic. We present several alternative translations, discuss their differences, and evaluate them on benchmarks that arise from 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.
Sun 16 JanDisplayed time zone: Eastern Time (US & Canada) change
15:05 - 16:35 | |||
15:05 30mPaper | Generalized Arrays for Stainless FramesRemote VMCAI | ||
15:35 30mPaper | NP Satisfiability for Arrays as PowersInPerson VMCAI | ||
16:05 30mPaper | Bit-Precise Reasoning via Int-BlastingRemote VMCAI Yoni Zohar Bar Ilan University, Ahmed Irfan Stanford University, Makai Mann Stanford University, Aina Niemetz Stanford University, Andres Nötzli Stanford University, USA, Mathias Preiner Stanford University, Andrew Reynolds University of Iowa, Clark Barrett Stanford University, Cesare Tinelli University of Iowa |