一句话：将抽象实现为程序变换，用 CEGAR 调节精度，并复用现成验证组件。
程序正确性证明常依赖抽象，但现有抽象实现难以复用与组合，成功技术往往需在新工具中反复重写。本文提出工具 CEGAR-PT，将抽象视为程序变换，并在不修改现有验证组件实现的前提下，把不同的现成验证组件集成起来，同时沿用 CEGAR 方法调节抽象精度。其抽象具有较强通用性：给定定义抽象层次的精度，只需将程序变换为另一程序；变换可对数据流做上近似（如 havoc 变量、使用更抽象类型），也可对控制流做上近似（如循环抽象、切片）。作者通过演示视频展示该工具。
Abstraction is an important approach for proving the correctness of computer programs. There are many implementations of this approach available, but unfortunately, the various implementations are difficult to reuse and combine, and the successful techniques have to be re-implemented in new tools again and again. We address this problem by contributing the tool cegar-pt, which views abstraction as program transformation and integrates different verification components off-the-shelf. The idea is to use existing components without having to change their implementation, while still adjusting the precision of the abstraction using the successful CEGAR approach. The approach of cegar-pt is largely general: It only restricts the abstraction to transform, given a precision that defines the level of abstraction, one program into another program. The abstraction by program transformation can over-approximate the data flow (e.g., havoc some variables, use more abstract types) or the control flow (e.g., loop abstraction, slicing). To illustrate our tool, we provide a demonstration video, accessible at https://youtu.be/ASZ6hoq8asE.