A Real-Blasting Extension of Cvc5 for Reasoning about Floating-Point Arithmetic
summary
An FPA solver is implemented as an extension to Cvc5 that real-blasting — translating floating-point formulas into a real-integer arithmetic (RIA) axiomatization — and uses lazy axiom instantiation via model-based refinement. The tool encodes conditional RIA axioms for operations (rounding, multiplication), enumerates models in Cvc5, checks concrete FP evaluations, and refines only failing cases. It outperforms bit-blasting on several bounded-model-checking benchmarks but shows ~15% unknowns/timeouts on others and can blow up when many axiom instances are generated.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 2:56Bit-blasting limitations
- 4:03Real-blasting motivation
- 7:44CVC5 implementation
- 13:51Tool workflow
- 18:35Benchmark setup
- 21:32Performance results
- 24:33Conclusion
- 25:30Q&A: Real-blasting advantages
- 26:57Q&A: Interaction with LRA
related talks
30mBit-Precise Reasoning via Int-Blasting
13mInteractive Bit Vector Reasoning using Verified Bitblasting
22mSatisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing
13mProgram Analysis via Efficient Symbolic Abstraction
01h 05mThe Power of Extended Resolution: A Practitioner's Perspective
58mPortable floating-point calculations
46mMechanizing Abstract Interpretation
19mSolving Floating-Point Constraints with Continuous Optimization