AI 中文总结
该研究对成熟工业C++代码库进行证明驱动软件理解，结合大语言模型、PVS和SeaHorn，对恒星区块链SDEX订单簿核心算法形式化分析，发现文档不一致，生成便于检查代码更改的工件，展示了定理证明与模型检查组合为遗留系统提供保证的途径。
AI 中文摘要
我们展示了一个关于对成熟的、安全关键型基础设施进行证明驱动软件理解的案例研究。虽然形式化方法传统上应用于设计阶段，但我们介绍了将形式化推理应用于成熟工业C++代码库的经验。我们专注于对实现恒星区块链SDEX订单簿的核心算法进行形式化分析。通过结合大语言模型（LLMs）、原型验证系统（PVS）和SeaHorn，我们能够证明生产代码库的核心属性。我们的方法还发现了与异常位置可达性相关文档中的不一致之处。最重要的是，我们生成了便于根据既定不变量检查代码更改的工件。这项工作展示了定理证明和模型检查的战略组合如何为向遗留系统提供强大保证提供一条途径。
英文摘要
We present a case study on proof-driven software understanding of mature, security-critical infrastructure. While formal methods are traditionally applied during the design phase, we present our experience applying formal reasoning onto a mature industrial C++ codebase. We focus on a formal analysis of the core algorithm that implements the Stellar blockchain's SDEX order book. By combining large language models (LLMs), Prototype Verification System (PVS), and SeaHorn, we are able to prove core properties of the production codebase. Our approach also identified an inconsistency in documentation related to the reachability of an exception location. Most importantly, however, we produce artifacts that make it easy for code changes to be checked against established invariants. This work demonstrates how the strategic combination of theorem proving and model checking provides a path for delivering robust assurance to legacy systems.
CommentsCAV 2026
