Sun 16 Jan 2022 16:05 - 16:35 at Salon I - Satisfiability Modulo Theories Chair(s): Natarajan Shankar

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 Jan

Displayed time zone: Eastern Time (US & Canada) change

15:05 - 16:35
Satisfiability Modulo TheoriesVMCAI at Salon I
Chair(s): Natarajan Shankar SRI International, USA
15:05
30m
Paper
Generalized Arrays for Stainless FramesRemote
VMCAI
Georg Stefan Schmid EPFL, Switzerland, Viktor Kunčak EPFL, Switzerland
15:35
30m
Paper
NP Satisfiability for Arrays as PowersInPerson
VMCAI
Rodrigo Raya EPFL, Viktor Kunčak EPFL, Switzerland
16:05
30m
Paper
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