交互式抽象解释：以低成本重新分析整个程序
摘要：交互式抽象解释的自动分析框架：从开发者角度提供静态程序分析 用于交互式抽象解释的框架，以方便软件开发者使用。尽管抽象解释本质上可以提供准确的分析结果，但通常代价很高。为了实现快速的响应时间，我们对分析基础设施进行了增量化处理，包括后处理，而无需对分析规范进行任何修改。我们依赖于局部通用的不动点引擎TD，该引擎动态跟踪依赖关系，同时探索对回答初始查询有贡献的未知因素。采用延迟失效来处理受程序更改影响的分析结果。特定改进支持增量分析并发缺陷，如数据竞争。该框架已在静态分析器Goblint中针对多线程C进行了实现，使用MagpieBridge将结果传递给IDE。我们根据响应时间和一致性的标准对实现进行评估：先前证明的不变性应保留-当它们不受更改影响时。结果表明，采用我们的方法，仅对小的更改进行重新分析所需的时间仅为从头开始分析时间的一小部分，同时大部分的准确性仍得以保留。我们还提供了程序开发的示例，突显整体方法的可用性。
作者：Julian Erhard, Simmo Saan, Sarah Tilscher, Michael Schwarz, Karoliine Holter, Vesal Vojdani, Helmut Seidl
论文ID：2209.10445
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-11-28