一句话：扩展 δ-决策过程以处理含积分的实数约束，并实现工具 ∫dReal 支持验证与合成。
许多程序合成与验证问题可归约为实数公式的可满足性判定，但这类公式常包含积分约束，现有 δ-决策过程无法直接处理。论文扩展 δ-决策过程框架，加入处理用户指定实函数积分的技术，并在 dReal 之上实现工具 ∫dReal。作者在一组基准上评估该工具，包括验证算法公平性、隐私机制的隐私与效用，以及为隐私机制合成满足目标效用的参数。实验性能表明 ∫dReal 能有效求解这些含积分约束的问题。
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}
}