Analyzing the Analyzers: Model Counting Meets Abstract Interpretation
The State Key Laboratory of Blockchain and Data Security, Zhejiang University（浙江大学区块链与数据安全全国重点实验室）
提出MCAI方法，利用模型计数量化抽象域的精度，通过符号抽象评估四个域的转换器精度，发现区间域精度接近八边形域，位级域优于字级域。
2026-06-23 cs.PL
Succinct Representations for Abstract Interpretation
抽象解释技术可以通过区分循环内的路径来变得更精确，代价是可能的指数复杂性。SMT解决技术和路径和路径集的稀疏表示避免了这个陷阱。我们改进了以前提出的技术指导静态分析和析取不变量的生成相结合的简洁表示的路径和符号表示的转换基于静态单分配的技术。由于扩展算子的抽象解释结果的非单调性，很难根据理论上的局部精度结果得出某个抽象比另一个抽象更精确的结论。因此，我们在各种开源软件包上对我们的新技术和以前的技术进行了广泛的比较。
2012-06-19 cs.PL
Abstract interpretation-based approaches to Security - A Survey on Abstract Non-Interference and its Challenging Applications
在本文中，我们提供了一个抽象的不干涉框架的调查。特别是，我们描述了一个一般形式化的抽象不干涉通过三个维度（观察，保护和语义），可以实例化，以获得众所周知的，甚至是新的削弱不干涉属性。然后，我们表明，在基于语言的安全性的概念，抽象的非干扰引入这种更一般的框架，它可以更好地理解的非干扰政策的不同组成部分的实例。最后，我们考虑两个具有挑战性的研究领域的安全性，抽象的非干扰似乎是一个很有前途的方法提供了新的观点和新的解决方案，开放的问题：代码注入和代码混淆。
2013-09-20 cs.PL
Mechanically Verified Calculational Abstract Interpretation
计算抽象解释（Calculational Abstract Interpretation）是一种由Cousot长期倡导的技术，用于从程序设计语言的形式语义中导出正确的构造抽象解释器。本文讨论了使用证明助手导出正确的构造验证抽象解释器的问题。我们确定了几个技术挑战，以克服的目的是支持验证计算抽象的解释，是忠实于现有的纸和纸的证明，支持计算与伽罗瓦连接一般，并使验证静态分析从这些证明提取。为了迎接这些挑战，我们开发了一个理论的伽罗瓦连接在一元风格，包括规格的影响。精确的计算可能是经典的推理，而纯计算具有可提取的计算内容。在规范和实现的世界之间移动是由我们的元理论实现的。为了验证我们的方法，我们给出了Cousot的“通用抽象解释器的计算设计”的第一个机械验证的正确性证明。“我们的证明“通过微积分”紧密遵循原来的纸笔证明，并支持提取一个验证过的静态分析器。
2015-07-13 cs.PL
Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis (Extended Version)
为了验证混合系统，我们扩展了抽象解释。摘要抽象在混合系统的验证方法中扮演着重要的角色，但对于常微分方程定义的连续动态的抽象需要特别注意。我们应用Cousot和Cousot的抽象解释框架的混合动力系统，几乎是因为它是，通过把连续动态无穷小离散跳跃的无限迭代。这种扩展遵循了Suenaga，Hasuo和Sekine最近的工作路线，其中演绎验证扩展为混合系统：1）为无穷小值引入常数dt; 2）采用Robinson的非标准分析（NSA）来定义数学上严格的语义。我们的理论结果包括健全性和终止通过统一加宽运营商和我们的原型实现成功地验证了一些基准的例子。
2015-11-03 cs.PL
Abstract Interpretation as a Programming Language
在David Schmidt的博士论文中，他探索了指称语义作为程序设计语言的使用。这是一项努力的一部分，不仅将形式语义视为规范，而且还将其视为编译器生成器的解释器和输入。语义本身可以被看作是一个程序，人们可以检查不同的编程风格和表示状态的方法。抽象解释主要是一种用于推导和规范程序分析的技术。与指称语义一样，我们也可以将抽象解释视为程序并检查其实现。本文的主要重点是表明，高阶严格性分析的结果可以更普遍地用作格上高阶函数的不动点算子，从而提供了一种立即实现一大类抽象解释的技术。此外，它可以被视为一种编程范式，并用于以循环风格编写程序。
2013-09-20 cs.PL
Abstract Interpretation under Speculative Execution
分析在支持推测执行的处理器上运行的程序的行为对于诸如执行时间估计和侧通道检测之类的应用是至关重要的。遗憾的是，现有的基于抽象解释的静态分析技术不对推测执行建模，因为它们关注程序的功能属性，而推测执行不改变功能。为了填补这一空白，我们提出了一种方法，使抽象的解释合理的投机执行。有两个贡献。首先，我们引入虚拟控制流的概念，以增加可能被推测执行的指令，从而影响后续指令。其次，为了使分析有效，我们提出了优化处理合并和循环，并安全地限制投机执行深度。我们已经实施和评估所提出的方法在静态高速缓存分析的执行时间估计和侧通道检测。我们的实验表明，新的方法，而保证是合理的投机执行下，优于国家的最先进的抽象解释技术，可能是不合理的。
2019-08-15 cs.PL
An Abstract Interpretation-based Model of Tracing Just-In-Time Compilation
跟踪即时编译是一种流行的动态语言编译技术，通常用于JavaScript、Python和PHP。我们提供了一个正式的模型跟踪JIT编译程序使用抽象解释。热路径检测对应于程序的跟踪语义的抽象。优化阶段对应于原始程序的转换，该转换保留其跟踪语义，直到通过某种抽象建模的观察。我们提供了一个通用的框架来表达动态优化，并证明他们是正确的。我们实例化它来证明动态类型特殊化和常量变量折叠的正确性。我们证明了我们的框架比Guo和Palsberg [2011]基于操作互模拟引入的跟踪编译模型更通用。
2015-10-28 cs.PL
Abstract Interpretation of Binary Code with Memory Accesses using Polyhedra
在本文中，我们提出了一种新的方法，静态分析的二进制代码使用抽象解释。我们使用一个抽象域的基础上多面体和两个映射函数，关联多面体变量与寄存器和内存。我们证明了我们的方法来计算上限的问题，循环迭代的代码。这个问题在安全关键实时代码的最坏情况执行时间（WCET）分析领域尤为重要。然而，我们的方法是通用的，它可以适用于其他静态分析问题。
2017-11-20 cs.PL
Decoupling the ascending and descending phases in Abstract Interpretation
抽象解释通过模仿程序在抽象域$\mathbb{A}$上的具体不动点计算来近似程序的语义。抽象（后）不动点计算通常分为两个阶段：上升阶段，使用加宽作为外推算子来强制终止，然后是下降阶段，使用展开作为插值算子，以减轻加宽引入的精度损失的影响。在本文中，我们提出了一个简单的变化，这种经典的方法，更有效地恢复精度，我们解耦的两个阶段：特别是，在开始下降阶段，我们取代域$\mathbb{A}$与更精确的抽象域$\mathbb{D}$。通过将其转换为A $^2$ I框架的实例，证明了该方法的正确性。在演示了一个简单的例子上的新技术后，我们总结了初步的实验评估的结果，表明它是能够获得显着的精度改进的几个选择的域$\mathbb{A}$和$\mathbb{D}$。
2022-06-22 cs.PL
Formal Verification of a C Value Analysis Based on Abstract Interpretation
基于抽象解释的静态分析器是实现精细算法的复杂软件。即使静态分析技术已经被很好地理解，它们在真实语言上的实现仍然容易出错。本文提出了一个使用Coq证明助手的形式化验证：一个基于抽象解释的价值分析的形式化，以及价值分析的可靠性证明。形式化依赖于泛型接口。机械化的证明是由一个布尔东克莱不动点迭代器的翻译验证。这项工作已被集成到CompCert验证的C编译器。我们的验证分析直接操作的编译器的中间语言具有相同的表达能力为C。我们的价值分析到OCaml的自动提取产生了一个具有竞争力的结果的程序，从实验中获得的一些基准和比较的框架-C工具。
2013-04-12 cs.PL
Deriving Escape Analysis by Abstract Interpretation: Proofs of results
面向对象语言的逃逸分析近似于不从给定上下文逃逸的对象集。如果我们把一个方法作为上下文，非转义对象可以在它的激活堆栈上分配;如果我们把一个线程作为上下文，那么就不需要在这些对象上使用Java同步锁。在本文中，我们形式化的基本逃逸域E作为一个抽象的解释具体的国家，我们然后细化到一个抽象的域ER比E更具体，因此，导致更精确的逃逸分析比E。我们提供的最优性结果为E和ER，在形式的伽罗瓦插入从具体的抽象域和最佳的抽象操作。伽罗瓦插入属性是通过使用抽象垃圾收集器将抽象域限制为不包含垃圾的那些元素而获得的。因此，我们实现的er是一个正式正确的转义分析器的实现，能够检测Java（字节码）应用程序的堆栈可分配创建点。这份报告包含了一篇论文的结果的证明，该论文具有相同的标题和作者，并将发表在《高阶符号计算》杂志上。
2006-07-28 cs.PL
A family of abstract interpretations for static analysis of concurrent higher-order programs
我们开发了一个框架，计算两个基本的分析并发高阶程序：（控制）流分析（CFA）和可能发生的并行分析（MHP）。我们特别关注的独特挑战所带来的不受限制的混合一流的延续和动态生成的线程。为了设置阶段，我们制定了一个具体的模型并发高阶程序：P（CEK*）S机。我们发现，这台机器的系统抽象的解释是能够计算流量和MHP分析。然而，仔细检查发现，MHP的精度很差。作为一种补救措施，我们采用了形状分析技术单例抽象动态产生的线程（而不是堆中的对象）。然后，我们表明，如果MHP分析是不感兴趣的，我们可以大大加快计算流分析单独崩溃线程交织与第二层的抽象。
2011-06-14 cs.PL
Completeness in static analysis by abstract interpretation, a personal point of view
本文从个人视角探讨了抽象解释静态分析中较少被关注的完备性要求，梳理了研究者多年来遇到的相关实际问题与疑问，补充了该领域除可靠性之外的研究视角。
2024-12-10 cs.PL
Correctness Witness Validation by Abstract Interpretation
本文提出一种新颖的抽象操作 unassume，通过将见证不变式纳入抽象程序状态以加速不动点收敛并提升精度，实现了通过抽象解释验证正确性见证，显著减少了多线程程序验证的 CPU 时间并能验证原本无法验证的属性。
2023-10-25 cs.PL
Property-Directed Reachability as Abstract Interpretation in the Monotone Theory
推导归纳不变量是形式化验证的主要挑战之一。抽象解释理论为设计不变推理算法提供了一个丰富的框架。不变推理的最新突破之一是属性导向可达性（PDR），但研究界认为PDR和抽象解释大多是不相关的技术。本文表明，令人惊讶的是，命题PDR可以制定为一个抽象的解释算法在逻辑域。更准确地说，我们定义了一个版本的PDR，称为$Λ$ -PDR，其中所有的反例的推广被用来加强一个框架。通过这种方式，不需要在创建框架后对其进行优化，因为所有可能的支持事实都已预先包含在内。我们分析这个算法使用的概念从Bshouty的单调理论，最初开发的背景下，精确的学习。我们发现，有一个固有的过度近似算法的框架之间的单调理论。然后，我们定义了一个新的抽象域，其中最好的抽象Transformer执行这种过近似，并表明它捕获了不变的推理过程，即，$Λ$ -PDR对应于在该抽象域中具有最佳Transformer的Kleene迭代。我们提供了一些充分的条件，当这个过程收敛在一个小的迭代次数，有时是一个指数差距所需的天真的精确向前可达的迭代次数。这些结果为PDR如何解决前向可达性的好处提供了坚实的理论基础。
2022-01-18 cs.PL
Sound, Precise, and Fast Abstract Interpretation with Tristate Numbers
扩展伯克利包过滤器（BPF）是一种语言和运行时系统，允许非超级用户通过将用户代码下载到内核中来扩展Linux和Windows操作系统。为了确保用户代码在内核上下文中安全运行，BPF依赖于一个静态分析器来证明代码的属性，例如有界内存访问和不存在崩溃的操作。BPF静态分析器使用具有多个抽象域的抽象解释来检查安全性。其中，tnums（三态数）域是用于推理程序值中的按位不确定性的关键域。本文对tnum抽象域及其算术运算符进行了形式化的定义。我们首次证明了BPF分析器中使用的tnum加法和减法抽象算术运算符的合理性和最优性。此外，我们还描述了一种新的tnum乘法算法，它比Linux内核的算法更精确、更高效（平均运行速度快33%）。我们的tnum乘法现在合并到Linux内核中。
2021-12-15 cs.PL
Flow-Sensitive Composition of Thread-Modular Abstract Interpretation
我们提出了一个基于约束的流敏感的静态分析并发程序通过迭代组成线程模块化的抽象解释器，通过使用一个系统的轻量级约束。我们的方法是组合的，因为它首先将顺序抽象解释器应用于各个线程，然后组合它们的结果。它是流敏感的，因为干扰的因果关系排序（从全局写入到读取的数据流）是由约束系统建模的。这些干扰约束是轻量级的，因为它们只涉及程序语句的执行顺序，而不是它们的数值属性：它们可以使用现成的数据库引擎有效地决定。我们的新方法的优势是更准确的比现有的，流不敏感的，静态分析，同时保持可扩展性，并提供预期的健全性和终止保证，即使是无限数据的程序。我们实现了我们的方法，并在大量的基准测试中进行了评估，证明了它在提高线程模块化抽象解释的准确性方面的有效性。
2017-09-28 cs.PL
Automating Abstract Interpretation of Abstract Machines
静态程序分析对于人们编写程序所使用的任何程序设计语言来说都是一种有价值的工具。脚本语言在世界上的流行表明，程序设计语言解释器相对容易编写。这些语言的用户抱怨他们没有能力分析他们的代码，因此程序设计语言分析器并不容易编写。本文研究了一种从传统解释器生成抽象解释器的系统方法，称为抽象抽象机。由于技术、理论和语用问题，抽象口译员很难发展。技术问题包括工程数据结构和算法。我表明，适度和简单的变化，抽象机器的数学表示的结果，在1000倍更好的运行时间-只是几秒钟的中等大小的程序。在理论领域，抽象会使正确性难以确定。我提供了证明技术，通过将计算能力留给外部因素：分配来证明抽象计算的常规、下推和堆栈检查下推模型的正确性。即使我们不信任证明，我们也可以针对测试套件具体地运行模型，以更好地信任它们。在务实的领域，我表明，抽象的抽象机器的系统过程是自动化的。我开发了一种类似于其他语义工程语言的用于表达抽象机器的元语言。该语言的特殊之处在于它提供了一个抽象分配的接口。语义保证，如果分配是有限的，那么语义是一个可靠的和可计算的近似的具体语义。
2015-04-29 cs.PL
Evaluation of the Implementation of an Abstract Interpretation Algorithm using Tabled CLP
CiaoPP是Ciao Prolog系统中逻辑程序的分析器和优化器。它包括PLAI，一个不动点算法的抽象解释的逻辑程序，我们适应使用表格约束逻辑编程。在这种适应中，制表引擎驱动定点计算，而约束求解器处理不同子句的抽象替换的LUB。这简化了代码并提高了性能，因为终止，依赖关系和一些关键操作（例如，分支切换和恢复）由制表引擎直接处理。确定是否已经达到不动点使用语义等价，这可以决定两个语法不同的抽象替换表示抽象域中的同一元素。因此，与使用语法相等的分析器相比，制表分析器可以在更多情况下重用答案。这有助于实现更好的性能，即使考虑到与这些检查相关的额外成本。我们的实现基于Ciao Prolog中的TCLP框架，并且是CiaoPP中初始定点实现的三分之一大小。它的性能进行了评估，通过分析几个程序使用不同的抽象域。这篇论文正在考虑发表在《逻辑程序设计理论与实践》（TPLP）上。
2019-07-31 cs.PL
Improving Thread-Modular Abstract Interpretation
我们给线程模块化的非关系值分析作为本地跟踪语义的抽象。语义以及分析制定的全球不变量和副作用的约束系统。我们表明，概括的静态分析仪Goblint提供的分析，以及一个自然的改进安托万Miné的方法，可以得到这个一般计划的实例。我们表明，这两个分析是无与伦比的w.r.t.精确度，并提供在精确度方面都有所改进的细化。我们还报告了一个初步的实验比较给定的分析一套有意义的基准。
2021-08-17 cs.PL
Generalized Strong Preservation by Abstract Interpretation
标准的抽象模型检验依赖于抽象Kripke结构，该结构通过将不可区分的状态粘合在一起来近似具体模型，即通过具体状态空间的划分。规约语言L的强保持性描述了L中公式的具体和抽象模型检验的等价性。我们展示了如何抽象的解释可以用来设计抽象模型，更一般的抽象Kripke结构。相应地，强保持被推广到基于抽象解释的模型，并与抽象解释中的完整性概念精确相关。最小化精化抽象模型以使其对某种语言L强保持的问题可以表述为抽象解释中的最小域精化以获得w.r.t. L的逻辑/时态运算符。结果表明，这个精炼的强保持抽象模型总是存在的，并且可以被刻画为一个最大不动点。因此，一些著名的行为等价，如互模拟，模拟和口吃，以及它们相应的分区细化算法可以优雅地在抽象解释为完整性属性和细化。
2006-03-14 cs.LO cs.PL
Clustered Relational Thread-Modular Abstract Interpretation with Local Traces
我们构建了新的线程模块化分析，跟踪关系信息的潜在重叠集群的全局变量-考虑到他们是由共同的互斥锁保护。我们提供了一个框架，系统地提高聚类关系分析的精度，通过分裂控制位置的基础上抽象的本地痕迹。作为一个实例，我们获得了动态线程创建和连接的分析。有趣的是，为全局变量跟踪较少的关系信息可能会导致更高的精度。我们考虑一类包含许多弱关系域的2-可分解域（例如，八角形）。对于这些域，我们证明，已经达到最大精度的集群的大小最多为2的全局。
2023-01-16 cs.PL
Interactive Abstract Interpretation: Reanalyzing Whole Programs for Cheap
为了使静态程序分析在软件开发人员的指尖，我们提出了一个框架的交互式抽象解释。虽然提供了合理的分析结果，但抽象解释通常可能非常昂贵。为了实现快速的响应时间，我们增加了分析基础设施，包括后处理，而不需要对分析规范本身进行任何修改。我们依赖于本地通用定点引擎TD，它动态跟踪依赖关系，同时探索有助于回答初始查询的未知数。对受程序变化影响的分析结果采用惰性失效方法。专门的改进支持并发缺陷（如数据竞争）的增量分析。该框架已在静态分析器Goblint中为多线程C实现，使用MagpieBridge将发现中继到IDE。我们评估我们的实施w.r.t.响应时间和一致性的标尺：以前证明的不变量应该被保留-当它们不受变化的影响时。结果表明，与我们的方法，小的变化后的重新分析只需要一小部分的从头开始的分析时间，而大部分的精度被保留。我们还提供了程序开发的例子，突出了整体方法的可用性。
2022-11-25 cs.PL
Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation
University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）
本文提出Evolving Abstract Transformer，通过UPOSE和AGG算法解决传统抽象解释的局限性，实现跨领域、高效精度-效率权衡和更精确的不变量。
2026-04-25 cs.PL
Reachability-based Acyclicity Analysis by Abstract Interpretation
在具有存储器的动态使用的程序设计语言（诸如Java）中，知道引用变量x指向非循环数据结构对于终止和资源使用的分析是有价值的（例如，执行时间或存储器消耗）。例如，对于x的任何字段f，该信息保证x所指向的数据结构的深度大于x.f所指向的数据结构的深度。这反过来又允许限制循环的迭代次数，该循环通过其深度遍历结构，这对于证明终止或推断循环的资源使用是必不可少的。本文提出了一种基于抽象解释的静态分析的形式化方法，用于推断非循环性，该方法基于两个抽象域的约简积：可达性，它模拟了变量w所指向的位置可以通过解引用另一个变量v而到达的性质（在这种情况下，v被称为到达w）;以及循环性，对v可以指向循环数据结构的属性进行建模。分析被证明是健全的和最佳的相对于所选择的抽象。
2013-02-13 cs.PL
Optimal Program Synthesis via Abstract Interpretation
University of Pennsylvania（宾夕法尼亚大学）
本文提出了一种基于抽象解释的框架，用于在领域特定语言中高效合成最优程序，通过A*搜索和抽象转换器提升可扩展性。
2026-02-16 cs.PL
Abstract Interpretation of Supermodular Games
超模博弈在各种模型中有着重要的应用，特别是在运筹学和非合作博弈论的经济应用中，并且具有完全格上多值函数不动点的纯策略纳什均衡。纯策略纳什均衡的supermodular游戏在这里近似诉诸理论的抽象解释，一个完善的和已知的框架，用于设计静态分析的程序设计语言。这是通过扩展理论的抽象解释，以处理近似的多值函数，并通过提供一些方法抽象supermodular游戏，以获得近似的纳什均衡被证明是正确的抽象解释框架内。
2015-07-06 cs.GT cs.PL
Optimism in Equality Saturation
University of California, Berkeley（加州大学伯克利分校）
本文提出了一种乐观的等价类分析算法，通过解决等价图表示中的微妙问题，提升了等价饱和过程的精度与效率。
2026-04-16 cs.PL
Correctness Kernels of Abstract Interpretations
在基于抽象解释的静态分析中，近似是由抽象域编码的。它们为设计抽象语义函数提供了系统的指导，这些抽象语义函数近似于分析中的某些具体系统行为。为了近似给定的具体语义功能，抽象域可能包含冗余信息。本文介绍了抽象解释的正确性核的概念，一种简化抽象域的方法，即从它们中删除抽象值，以最大的方式，同时保留完全相同的近似行为的系统分析。我们表明，在抽象的模型检验正确性内核提供了一个由示例指导的抽象状态空间的简化范例，这意味着这种简化保留了示例的虚假性（即，抽象路径）。特别是，我们展示了如何正确的内核可以集成与著名的CEGAR（反例引导的抽象细化）方法。
2013-04-19 cs.LO cs.PL
Deriving Abstract Interpreters from Skeletal Semantics
本文提出一种基于骨架语义及其语义元语言抽象解释的方法，从编程语言形式化语义派生可执行抽象解释器，并通过小型命令式语言的值分析验证了其通用性与正确性。
2023-09-13 cs.PL
SEA: String Executability Analysis by Abstract Interpretation
动态语言通常使用反射原语在运行时将动态生成的文本转换为可执行代码。这些特征使得标准的静态分析即使不是不可能的，也是极其困难的，因为其基本的数据结构，即，与要分析的程序相关联的控制流图和递归方程系统本身是动态变化的对象。我们介绍SEA，一个抽象的解释器，用于自动的声音字符串可执行性分析的动态语言采用有界（即嵌套）反射和动态代码生成。字符串静态近似在一个抽象域的有限状态自动机的基本操作实现为符号转换器。SEA将标准程序分析与字符串可执行性分析结合在一起。对反射调用的分析确定了对同一个抽象解释器的调用，该抽象解释器是直接从该程序点的静态字符串可执行性分析的结果合成的代码。使用正则语言来近似动态生成的代码结构，使得SEA能够合理地近似自修改程序的安全属性，同时保持效率。这里的合理性意味着分析器为解决反射而合成的代码的语义过度近似于程序在运行时动态构建的代码的语义。
2017-02-08 cs.PL
Injecting Abstract Interpretations into Linear Cost Models
我们提出了一个基于语义的框架，用于分析程序的资源使用的定量行为。我们从一个带有成本的操作语义开始。成本集的双曲面结构允许将定量语义定义为线性算子。然后，我们提出了一个抽象的抽象技术的启发，从抽象的解释，以有效地计算全局成本信息的程序。抽象必须考虑两个不同的顺序概念：成本顺序和状态顺序。我们表明，我们的抽象技术提供了一个正确的近似的具体成本计算。
2010-06-26 cs.LO cs.PL
Abstract Interpretation for Generalized Heuristic Search in Model-Based Planning
Massachussetts Institute of Technology（麻省理工学院）
基于模型的领域通用规划者通常通过放松或抽象符号世界模型来构建搜索策略，从而获得其通用性。我们说明了如何抽象的解释可以作为一个统一的框架，这些抽象为基础的启发式搜索，扩展范围的启发式搜索更丰富的世界模型，利用更复杂的数据和功能（如集，几何），甚至模型的不确定性和概率的影响。这些理论也可以与学习相结合，允许代理通过抽象派生的信息在新的世界模型中快速启动规划，这些信息后来通过经验进行了改进。这表明抽象解释在构建通用推理系统中可以发挥关键作用。
2022-08-05 cs.AI cs.PL
Abstract Interpretation-Based Data Leakage Static Analysis
本文提出一种基于抽象解释的静态分析方法，可在开发阶段提前检测机器学习中的数据泄漏，并在 NBLyzer 框架中实现，在 2000 多个 Kaggle notebook 上验证了其有效性和精度。
2024-08-06 cs.PL
Towards Cumulative Abstract Semantics via Handlers
University of Colorado Boulder（科罗拉多大学博尔德分校）；Amazon（亚马逊）
本文提出通过作用域效应实现累积抽象语义，以构建模块化且优雅的抽象解释框架。
2026-02-17 cs.PL
Sound Symbolic Execution via Abstract Interpretation and its Application to Security
符号执行是一种程序分析技术，通常用于确定程序是否违反属性，并在发现违反的情况下生成可以触发它们的输入。在不干扰等安全属性的上下文中使用，当发现不安全的信息流时，符号执行在寻找反例对时是精确的，但是它只在一定范围内是合理的，因此它不允许证明执行超出给定范围的程序的正确性。相比之下，基于抽象解释的静态分析保证了可靠性，但通常缺乏提供反例迹对的能力。在本文中，我们建议编织两者以获得两个世界中最好的。我们通过一系列静态分析证明了这一点，包括一个名为RedSoundRSE的静态分析，旨在验证非干扰性。RedSoundRSE既提供了语义上合理的结果，也提供了导出一个边界内的反例对的能力。它依赖于符号执行和抽象域的组合，灵感来自于众所周知的简化产品概念。我们形式化RedSoundRSE，并证明其合理性以及其相对精度达到一个界限。我们还提供了RedSoundRSE的原型实现，并在具有挑战性的示例样本上对其进行评估。
2023-01-18 cs.PL
Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
提出基于抽象解释的自动机参数化依赖效应分析，用于递归高阶程序时序安全验证，原型 evDrift 在 23 个基准中验证 21 个并显著优于既有工具。
2025-08-30 cs.PL
A Categorical Framework for Program Semantics and Semantic Abstraction
本文提出一种用于抽象解释的函子方法，将解释表示为偏序集范畴中的oplax函子，并用lax自然变换表示抽象关系，从而将函子语义的优势引入语义抽象并讨论了其健全性。
2023-11-18 cs.PL math.CT
Abstracting Abstract Machines
我们描述了一种推导的方法，抽象的解释，产生新颖的和透明的声音静态分析时，适用于完善的抽象机器。为了证明的技术和支持我们的要求，我们转换的CEK机Felleisen和弗里德曼，Krivine的机器的懒惰的变种，和堆栈检查CM机克莱门茨和Felleisen到抽象的解释自己。由此产生的分析约束时序的程序事件，预测返回流和堆栈检查行为，并近似的流量和评估的需要参数。对于所有这些机器，我们发现，一系列众所周知的具体的机器重构，加上我们称之为存储分配延续的技术，导致机器抽象到静态分析简单地通过绑定其存储。我们证明了该技术的规模统一，允许静态分析现实的语言功能，包括尾部调用，条件，副作用，异常，一流的延续，甚至垃圾回收。
2010-09-07 cs.PL
Abstract Program Slicing: an Abstract Interpretation-based approach to Program Slicing
在本文中，我们正式定义了抽象程序切片的概念，程序切片的一般形式被认为是数据的属性，而不是它们的确切值。这种方法适用于具有数值和引用值的语言，并依赖于程序组件（语句）之间的抽象依赖关系的概念。不同形式的（后向）抽象切片被添加到现有的正式框架中，传统的非抽象形式的切片可以进行比较。扩展的框架使我们能够理解抽象切片是传统切片的推广，因为传统切片（处理语法依赖关系）是由（语义）非抽象形式的切片推广的，这实际上相当于对数据执行身份抽象的抽象形式。声音算法计算抽象的依赖关系和程序片的系统表征，它依赖于程序状态之间的协议的概念。
2016-05-17 cs.LO cs.PL
Sequence-Based Abstract Interpretation of Prolog
针对现有Prolog抽象解释框架无法覆盖部分控制结构的问题，提出基于替换序列、可处理深度优先搜索与cut操作符的新框架，证明其适配传统抽象域且可涵盖此前的确定性分析工作，实验验证了有效性。
2000-10-19 cs.LO cs.PL
Systematic Abstraction of Abstract Machines
我们描述了一个派生的方法，抽象的解释，产生新颖的和透明的声音静态分析时，适用于高阶和命令式程序设计语言完善的抽象机器。为了证明的技术和支持我们的要求，我们转换的CEK机Felleisen和弗里德曼，Krivine的机器的懒惰的变种，和堆栈检查CM机克莱门茨和Felleisen到抽象的解释自己。由此产生的分析约束时序的程序事件，预测返回流和堆栈检查行为，并近似的流量和评估的需要参数。对于所有这些机器，我们发现，一系列众所周知的具体的机器重构，加上存储分配的延续技术，导致机器抽象到静态分析简单地通过绑定他们的商店。我们证明了该技术的规模统一，允许静态分析现实的语言功能，包括尾部调用，条件，副作用，异常，一流的延续，甚至垃圾回收。为了缩小形式主义和实现之间的差距，我们将数学翻译为运行Haskell代码，用于我们方法的初始开发。
2011-07-18 cs.PL
Abstract Interpretation with Unfoldings
我们提出并评估了一种技术，用于计算路径敏感的并发程序的抽象解释过程中的干扰条件。代替不动点计算，我们使用素事件结构来compensate表示因果关系的依赖性和干扰之间的序列的变压器。我们的主要贡献是一个展开算法，使用一个新的概念的独立性，以避免冗余的Transformer应用程序，线程本地固定点，以减少展开的大小，和一个新的截断标准的基础上包容，以保证终止的分析。我们的实验表明，抽象展开产生一个数量级的假警报比一个成熟的抽象解释器，而几个数量级的速度比求解器为基础的工具，具有相同的精度。
2017-05-01 cs.LO cs.PL
A New Numerical Abstract Domain Based on Difference-Bound Matrices
本文通过抽象解释提出了一种新的静态分析数值抽象域。这个域允许我们表示形式为（x-y<=c）和（+/-x<=c）的不变量，其中x和y是变量值，c是整数或实常数。抽象元素用差分定界矩阵表示，广泛应用于模型检查器，但我们必须设计新的操作符来满足抽象解释的需要。其结果是一个完整的无限高的晶格具有扩大，缩小和共同的传递函数。我们专注于给出一个有效的O（n2）表示和基于图的O（n3）算法-其中n是变量的数量|并声称该域总是比公知的区间域执行得更精确。为了说明这个领域的精度/成本权衡，我们已经实现了简单的抽象解释器玩具命令和并行语言，使我们能够证明一些非平凡的算法正确。
2007-03-16 cs.PL
Worst-Case Groundness Analysis Using Definite Boolean Functions
本说明说明了理论上的最坏情况下的情况下，通过抽象的解释明确（Def）和积极的（Pos）布尔函数的抽象域的接地分析。对于Def，给出了一个例子，其中任何基于def的抽象解释的接地分析如下的链是指数的参数位置的数量，以及在条款的数量，但次指数的大小的程序。对于POS，我们加强了以前的结果，说明了一个例子，其中任何基于POS的抽象解释接地分析如下的链是指数的大小的程序。确定Def的最坏情况是否真的和Pos一样糟糕仍然是一个悬而未决的问题。
2004-05-27 cs.PL
Combining Forward and Backward Abstract Interpretation of Horn Clauses
前向分析和后向分析的交替是程序抽象解释中的一种标准技术，当我们希望证明某些不需要的程序状态不可达时，这种技术特别有用。当前用于组合Horn子句的前向（在逻辑编程术语中为自底向上）和后向（自顶向下）抽象解释的最先进技术是查询-应答转换。它转换了Horn子句系统，使得标准的前向分析可以从目标向前和向后传播约束。问答转换是有效的，但有我们希望解决的问题。为此，我们引入了一个新的后向收集语义，它适用于交替的前向和后向抽象解释的Horn子句。我们展示了如何交替可以用来证明无法达到的目标，以及如何每一个后续运行的分析产生一个完善的系统模型。实验上，我们观察到，结合向前和向后的分析是很重要的分析系统编码的问题，在C程序的可达性。特别是，遵循我们的新语义的组合提高了我们自己的抽象解释器的精度，包括与查询-答案转换系统的前向分析相比。
2017-08-07 cs.LO cs.PL
Combining E-Graphs with Abstract Interpretation
本文提出将 e-graph 等价性饱和与抽象解释紧密耦合，利用抽象性质启用条件重写规则，并通过等价聚类提升抽象精度，同时给出区间算术实现并在 FPBench 上验证。
2023-08-15 cs.DS cs.PL
Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday
这本书是一本散文集，从个人回忆到技术贡献。这是对戴夫·施密特和他的职业生涯的致敬，并在他六十岁生日之际创作。
2013-09-18 cs.LO cs.PL cs.SE
Absynthe: Abstract Interpretation-Guided Synthesis
本文提出语言无关的 Absynthe，用用户自定义抽象语义引导搜索并以具体测试验证，在 SyGuS 与 Pandas 基准上达到具竞争力结果。
2023-04-24 cs.PL
An Experiment Combining Specialization with Abstract Interpretation
以前的研究表明，控制流细化可以通过一个程序专门化结合基于属性的抽象来实现，以提高终止和复杂性分析工具。我们现在表明，这个专门构建的专门化程序可以以更模块化的方式进行重构，并且可以使用现成的部分评估工具来实现先前的结果，并将其应用于抽象解释器。抽象解释器的关键特征是抽象域，它是基于属性的抽象域与具体域的乘积。这种独立于语言的框架提供了一种实用的方法来实现各种强大的专门化，并有助于使用解释器和专门化来实现程序转换的研究。
2020-08-07 cs.LO cs.PL cs.SC
Improving Dynamic Code Analysis by Code Abstraction
在本文中，我们的目标是提出一个模型的代码抽象，抽象解释的基础上，使我们能够提高最近提出的动态语言的抽象解释的静态分析的精度。我们在这里解决的问题是，分析可能会向string-to-execute抽象值添加一些虚假代码，并且这些代码可能需要一些抽象表示才能使其可分析。这正是我们在这里提出的，我们通过必须执行的分析来驱动代码抽象。
2021-09-07 cs.PL cs.SE
An Abstract Monte-Carlo Method for the Analysis of Probabilistic Programs
本文介绍了一种新的方法，随机测试和抽象解释相结合，用于分析具有概率和非概率不确定性的程序。在介绍了“普通”测试后，我们展示了如何将测试和抽象解释相结合，并给出了将结果的精度与迭代次数联系起来的公式。然后，我们讨论了复杂性和优化问题，并结束了一些实验结果。
2007-01-30 cs.PF cs.PL
Quantum entanglement analysis based on abstract interpretation
纠缠是量子态的一种非定域性质，在量子信息论中起着决定性的作用。一些协议，如隐形传态，是基于量子纠缠态。此外，任何不产生纠缠的量子算法都可以在经典计算机上有效地模拟。然而，纠缠的确切作用还没有得到很好的理解。由于纠缠演化的精确分析会导致指数减速，我们考虑基于抽象解释框架的近似分析。本文将一种基于超算子的具体量子语义与一种简单的量子程序设计语言联系起来。纠缠的表示，即抽象域的设计是一个关键问题。选择纠缠作为存储器的分区的表示。一个抽象的语义介绍，并证明了近似的可靠性。
2008-01-28 cs.LO cs.PL quant-ph
