法律合同形式化验证：基于翻译的方法（扩展版）
软件工程
2025-09-29 v2
摘要
Stipula 是一种专用于建模具有可执行属性的法律合同的域特定编程语言，尤其是涉及资产转移和义务的合同。本文提出一种通过将 Stipula 合同翻译为带有 Java Modeling Language 规范注释的 Java 代码来对 Stipula 合同的正确性进行形式化验证的方法。作为验证后端，使用演绎验证工具 KeY。该翻译和对大型 Stipula 合同（具有不相交循环）的部分正确性和总正确性的验证完全自动化。我们的工作表明，通用性的演绎验证工具在翻译方法中可以成功应用。
引用
@article{arxiv.2509.20421,
title = {Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)},
author = {Reiner Hähnle and Cosimo Laneve and Adele Veschetti},
journal= {arXiv preprint arXiv:2509.20421},
year = {2025}
}