Book chapter
Bit-Precise Reasoning via Int-Blasting
Verification, Model Checking, and Abstract Interpretation, pp.496-518
Lecture Notes in Computer Science, Springer International Publishing
01/14/2022
DOI: 10.1007/978-3-030-94583-1_24
Abstract
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.
Details
- Title: Subtitle
- Bit-Precise Reasoning via Int-Blasting
- Creators
- Yoni Zohar - Bar-Ilan UniversityAhmed Irfan - Stanford UniversityMakai Mann - Stanford UniversityAina Niemetz - Stanford UniversityAndres Nötzli - Stanford UniversityMathias Preiner - Stanford UniversityAndrew Reynolds - University of IowaClark Barrett - Stanford UniversityCesare Tinelli - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Verification, Model Checking, and Abstract Interpretation, pp.496-518
- Publisher
- Springer International Publishing; Cham
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-030-94583-1_24
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 01/14/2022
- Academic Unit
- Computer Science
- Record Identifier
- 9984259413202771
Metrics
10 Record Views