Checking δ-Satisfiability of Reals with Integrals

Many synthesis and verification problems can be reduced to determining the truth of formulas over the real numbers. These formulas often involve constraints with integrals in them. To this end, we extend the framework of 𝛿-decision procedures with techniques for handling integrals of user-specified real functions. We implement this decision procedure in the tool dReal, which is built on top of dReal. We evaluate dReal on a suite of problems that include formulas verifying the fairness of algorithms and the privacy and the utility of privacy mechanisms and formulas that synthesize parameters for the desired utility of privacy mechanisms. The performance of the tool in these experiments demonstrates the effectiveness of dReal. CCS Concepts: • Theory of computation → Logic and verification; • Security and privacy → Logic and verification; • Mathematics of computing → Integral equations; • Software and its engineering → Model checking.