Checking $\delta$-Satisfiability of Reals with Integrals
summary
Extends δ-decision procedures to handle integrals by implementing ∫dReal on top of dReal and combining IBEX interval propagation with the ARB arbitrary-precision ball integrator; proves δ-satisfiability decidability for a logic with nested and variable-bound integrals; evaluates on 41 benchmarks (fairness, privacy, synthesis) and matches exact results while beating Mathematica except on triple integrals; scales to 100 nested integrals (sum in 0.02s, product in 0.6s).
AI-written summary · about
chapters (11)
- 0:00Introduction
- 0:45Integrals in verification
- 2:17Delta decision procedure
- 3:43Key contributions
- 5:10Integral constraint propagation
- 7:27ARB for integral computation
- 8:32Tool architecture
- 9:38Benchmark vs Mathematica
- 10:46Scalability with nested integrals
- 11:50Future work
- 12:11Q&A
related talks
25mA Logic for the Imprecision of Abstract Interpretations
30mFormalization of Differential Privacy in Isabelle/HOL
06mDistribution Theoretic Semantics for Non-Smooth Differentiable Programming
24mThe Best of Abstract Interpretations
28mCertifying rings of integers in number fields
17mFormalizing Determinacy of Concurrent Revisions
01h 05mThe Power of Extended Resolution: A Practitioner's Perspective
30mBit-Precise Reasoning via Int-Blasting