Verifying relations between programs arises as a task in various verification contexts such as optimizing transformations, relating new versions of programs with older versions (regression verification), and noninterference. However, relational verification for programs acting on dynamically allocated mutable state is not well supported by existing tools, which provide a high level of automation at the cost of restricting the programs considered. Auto-active tools, on the other hand, require more user interaction but enable verification of a broader class of programs. This article presents WhyRel, a tool for the auto-active verification of relational properties of pointer programs based on relational region logic. WhyRel is evaluated through verification case studies, relying on SMT solvers orchestrated by the Why3 platform on which it builds. Case studies include establishing representation independence of ADTs, showing noninterference, and challenge problems from recent literature.

翻译：程序间关系的验证出现在多种验证场景中，如优化变换、新版本与旧版本程序的关联验证（回归验证）以及非干扰性。然而，对于作用于动态分配可变状态程序的关系验证，现有工具的支持并不充分——这些工具虽提供高度自动化，但以限制程序类型为代价。相比之下，自动化主动验证工具需要更多用户交互，但能处理更广泛的程序类别。本文提出WhyRel，一种基于关系区域逻辑、用于指针程序关系属性的自动化主动验证工具。通过基于Why3平台集成的SMT求解器编排，我们利用验证案例研究评估了WhyRel。案例涵盖抽象数据类型表示独立性证明、非干扰性验证以及近期文献中的挑战性问题。