Quantified Underapproximation via Labeled Bunches

doi:10.1145/3763051

2025-10-01

PRE

DOI：10.1145/3763051

原文求助

摘要

En 中文

鉴于形式验证的高成本，一个大型系统可能包含经过不同分析的组件：少数是全验证的，其余是测试的。目前，尚无能够可靠地组合这些异构分析并推导出整个系统整体形式保证的推理系统。传统的组合推理技术——依赖保证推理——对经历过度近似推理的验证组件有效，但对经历欠近似推理的组件无效，例如使用测试或其他程序分析技术。本文的目标是为组合异构分析开发一个形式化、逻辑化的基础，同时采用过度近似（验证）和欠近似（测试）推理。我们专注于可建模为通信进程集合的系统。每个进程拥有其内部资源和一组通过其与其他进程通信的通道。关键思想是量化关于进程行为在测试级别上获得的保证，该级别捕获保证被分析为真时所受的约束。我们设计了一个基于聚束蕴涵逻辑的新型证明系统LabelBI，该系统使得针对不同分析组件的系统能够应用依赖保证推理原则。我们为该逻辑开发了迹语义，并在此基础上证明了我们的逻辑是可靠的。我们还证明了我们的sequent演算的截断消除。我们通过一个案例研究展示了我们逻辑的表达能力。

Keyword:

Logic of bunched implication

Separation logic

Testing