Bit-Precise Reasoning via Int-Blasting
summary
Introduces int-blasting: translating bit-vector formulas to integer arithmetic plus uninterpreted functions and implementing four variants (eager/lazy × sum/bitwise) inside cvc5. Evaluated on ~40k QF_BV SMT-LIB cases, ~55k rewrite-rule candidates (10 widths each from 16 to 8192), and 35 real-world 256-bit smart-contract VCs. Shows int-blasting, especially the lazy bitwise mode, outperforms bit-blasting on large bit-widths (wins start around 512 bits) and solves the most of the 35 contract benchmarks; bit-blasting still wins on many SMT-LIB families.
AI-written summary · about
chapters (23)
- 0:00Introduction
- 0:18Presentation
- 0:44General Subject
- 1:45BitBlasting
- 2:56integerbased approach
- 4:08IntBlasting
- 6:39Translation function
- 8:25Arithmetic operators
- 9:09Shift operators
- 10:03Bitwise operators
- 10:22Implicit assumption
- 11:21Variants
- 12:00Eager Variance
- 12:41Sum Mode
- 13:40Gamma
- 15:16Delta
- 15:59Conclusion
- 16:59Comparison
- 17:56ST Label
- 18:11Rewrite Rules
- 19:02Benchmarks
- 19:30Results
- 22:37Discussion
related talks
13mInteractive Bit Vector Reasoning using Verified Bitblasting
29mA Real-Blasting Extension of Cvc5 for Reasoning about Floating-Point Arithmetic
20mBit Blasting Probabilistic Programs
01h 25mRISC V Bit Manipulation ISA Extension Spec, Hardware, Software
16mCertified Decision Procedures for Width-Independent Bitvector Predicates
19mSMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories
19mPanel: Compilation Frameworks
13mProgram Analysis via Efficient Symbolic Abstraction