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.

@article{paperbot3158,
  title = {Checking δ-Satisfiability of Reals with Integrals},
  author = {Cody Rivera and Bishnu Bhusal and Rohit Chadha and A. Prasad Sistla and Mahesh Viswanathan},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {OOPSLA1},
  year = {2025},
  doi = {10.1145/3720446}
}