paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Bringing Invariant Analysis to modern IDEs: The DIG+ Extension for VS Code

把不变式分析带入现代 IDE：面向 VS Code 的 DIG+ 扩展
ISSTA Proceedings of the 34th ACM SIGSOFT International Symposium on Software Testing and Analysis2025匹配度 4/10 · 该论文将不变式分析集成到 VS Code，属于程序分析与形式化验证/开发者工具方向，与用户对静态分析、形式化验证的一般兴趣相关；但未涉及 LLM/Agent、浮点程序分析或贝叶斯程序分析等核心交叉方向，也不是问题驱动的分析技术突破。引用 0 inbox
Stefania Piciorea, ThanhVu Nguyen
编程环境与开发者工具程序分析与抽象解释
crossref: 2026-09-12

AI 速览

一句话：为 VS Code 构建 DIG+ 扩展，将不变式分析集成到现代 IDE，降低传统工具的使用门槛。

程序不变式是在特定程序位置成立的性质，对形式化程序验证与分析很重要。现有的动态和静态不变式生成方法数量多且功能强大，支持广泛的应用。然而，这些工具通常因命令行接口复杂、需要专业技术知识而未被充分利用。DIG+ 扩展面向 VS Code，旨在将不变式分析能力带入现代 IDE，以改善可用性并降低使用门槛。摘要未报告具体实现细节与实验评估。

问题
现有不变式生成工具虽强大，却因复杂命令行接口和较高专业门槛而未被充分利用；如何让程序验证与分析中的不变式能力更易被开发者使用。
方法
通过为 VS Code 开发 DIG+ 扩展，将不变式分析集成到现代 IDE，以降低使用门槛。
评估
摘要未给出具体评估；仅从可用性与工具集成角度说明动机。
原文摘要（Abstract）

Program invariants, which are properties that hold at specific program locations, are important in formal program verification and analysis. Traditional invariant generation methods using dynamic and static analyses are abundant and powerful, supporting a wide range of applications. However, these tools often remain underutilized due to their complex command-line interfaces and the technical expertise required for usage.

链接与引用

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

BibTeX 
@inproceedings{paperbot9590,
  title = {Bringing Invariant Analysis to modern IDEs: The DIG+ Extension for VS Code},
  author = {Stefania Piciorea and ThanhVu Nguyen},
  booktitle = {ISSTA},
  year = {2025},
  doi = {10.1145/3713081.3731737}
}