本文提出了一种基于图论的自动化验证框架 GAuV，用于验证多方计算（MPC）协议在完美半诚实安全模型下的安全性。传统上，MPC 协议的安全性证明依赖于针对具体协议手工构造模拟器，并对其输出分布与真实世界损坏方视图进行理论分析，这一过程繁琐且容易出错。此外，即使协议在理论上是安全的，实现过程中的粗心也可能引入安全漏洞，且难以检测。GAuV 框架能够自动验证 MPC 协议实例的完美安全性，具有完全的可靠性（soundness）：任何通过该框架验证的协议，在模拟器定义的语义下也是安全的。作者还证明了框架的完备性，即对于任何 BGW 协议实例，该框架都能在多项式时间内验证其对于所有损坏方集合的安全性。与以往仅关注黑盒隐私（即损坏方输出不泄露诚实方输入信息）的工作不同，GAuV 有潜力用于验证任意 MPC 协议的安全性。作者实现了原型系统，评估显示原型能在合理时间内自动证明 BGW 协议和 B2A（二进制到算术）转换协议的完美半诚实安全性。该研究为 MPC 协议的安全性验证提供了自动化工具，有助于减少手工证明的复杂性和实现错误带来的风险。

本文提出 DPGen，一种面向差分隐私（Differential Privacy, DP）的自动程序合成方法。差分隐私已成为以隐私保护方式发布数据的实际标准，但设计一个满足差分隐私的算法通常需要从无噪声（非私有）算法出发，由设计者手动决定在何处添加噪声以及添加多少噪声。这一过程并不平凡，若处理不当，算法可能违反差分隐私或导致数据效用低下。DPGen 的核心目标是将这一繁琐且易出错的人工设计过程自动化：给定一个非私有算法以及隐私预算等约束，DPGen 自动合成一个满足差分隐私的版本，同时尽量保持较高的数据效用。该方法通过程序合成技术，在候选噪声插入策略与噪声量配置的搜索空间中寻找可行且最优的解。论文主要贡献包括：（1）形式化定义了从非私有算法到私有算法的自动合成问题；（2）设计了有效的合成算法，能够处理多种常见算法结构；（3）在多个基准任务上验证了所合成私有算法的效用与隐私保证。该研究适合对差分隐私机制自动化设计、程序合成以及隐私保护数据发布感兴趣的研究人员阅读。由于本文仅为摘要，尚无法获取实验细节与算法伪代码，但核心思想清晰：将差分隐私机制设计从手工过程转变为可自动搜索的合成问题。