paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Decomposing software verification into off-the-shelf components

将软件验证分解为现成组件
ICSE Proceedings of the 44th International Conference on Software Engineering2022匹配度 3/10 · 论文讨论软件验证技术的组件化复用与负载分配，属于程序验证/形式化验证的工程架构方向；但未涉及 LLM/Agent 改进验证、浮点程序分析或贝叶斯程序分析，与用户核心的 AI×PL 交叉方向仅弱相关。引用 18 inbox
Dirk Beyer, Jan Haltermann, Thomas Lemberger, Heike Wehrheim
程序验证
crossref: 2026-09-12

AI 速览

一句话：提出把软件验证技术拆分为更小、更专用的可复用现成组件，以促进复用与负载分配。

当前软件验证技术通常被实现为紧耦合的软件单体，各组件彼此依赖，导致难以复用，也限制了工作负载分配的能力。本文主张将验证功能分解为更小、更专用的现成组件，使这些组件可以被独立地重用与组合，并让验证工作负载能够在组件层面进行分配。作者认为，这种分解方式有助于软件验证领域的创新更快地转化为实践。摘要仅阐述了这一分解思路及其动机，属于立场/架构层面的论述，未给出具体的分解方案、组件接口或实验评估结果。

问题
软件验证技术以紧耦合单体形式实现，组件难以复用，且工作负载分配的潜力受到限制。
方法
提出将验证任务分解为更小、更专用的即用型组件，通过组件化与组合来支持复用并分配验证负载。
评估
摘要属于立场性/架构层面的论述，未报告具体实现或实验评估结果。
原文摘要（Abstract）

Techniques for software verification are typically realized as cohesive units of software with tightly coupled components. This makes it difficult to re-use components, and the potential for workload distribution is limited. Innovations in software verification might find their way into practice faster if provided in smaller, more specialized components.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot6925,
  title = {Decomposing software verification into off-the-shelf components},
  author = {Dirk Beyer and Jan Haltermann and Thomas Lemberger and Heike Wehrheim},
  booktitle = {ICSE},
  year = {2022},
  doi = {10.1145/3510003.3510064}
}