Abstract Neural Networks
University of California, Davis（加州大学戴维斯分校）
深度神经网络（DNN）正迅速应用于无人机和飞机控制等安全关键领域，激发了验证其行为安全性的技术。不幸的是，DNN验证是NP难的，当前的算法随着DNN中节点的数量呈指数级增长。本文介绍了抽象神经网络（ANN）的概念，它可以用来在使用较少节点的情况下完全过度逼近DNN。ANN类似于DNN，除了权重矩阵被给定抽象域中的值所取代。我们提出了一个由抽象域和DNN中使用的激活函数参数化的框架，可以用来构建相应的ANN。我们提出了DNN激活函数的必要和充分条件，以使所构建的ANN完全过逼近给定的DNN。先前关于DNN抽象的工作仅限于区间域和ReLU激活函数。我们的框架可以用其他抽象域（如八边形和多面体）以及其他激活函数（如Leaky ReLU、Sigmoid和Hyperbolic Tangent）来实例化。
2020-09-11 cs.LG cs.PL stat.ML
A Few Graph-Based Relational Numerical Abstract Domains
本文给出了一类非关系数值抽象域的系统设计。构造的域表示形式为（C中的vj - vi）的不变量的集合，其中vj和vi是两个变量，并且C存在于P（Z）、P（Q）或P（R）的抽象中。我们称这类域为弱关系域。允许这种建设的基本概念是潜在的图形和最短路径封闭算法在exotic-like代数的扩展。给出了示例构造，以检索知名的域以及新的。这样的域可以在抽象解释框架中使用，以便设计各种静态分析。这种结构的一个主要好处是它的模块化，允许快速实现新的抽象域从现有的。
2007-03-16 cs.PL
Program Analysis with Local Policy Iteration
我们提出了一种新的算法，用于推导数值不变量，结合了最大策略迭代的精度与传统Kleene迭代的灵活性和可扩展性。它在可配置程序分析（CPA）框架中定义，因此允许分析间通信。它使用可调块编码来遍历无循环的程序部分，可能包含分支，而不引入额外的抽象。我们的技术操作在任何模板线性约束域，包括区间和八角形域;模板也可以从程序源代码中导出。的实施进行了评估，从软件验证比赛（SV-Comp）的一组基准。它可以与最先进的分析仪竞争。
2015-11-03 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
Learning Abstractions for Program Synthesis
许多示例引导的程序合成技术使用抽象来修剪搜索空间。虽然基于抽象的合成已经被证明是非常强大的，但领域专家需要提供一个合适的抽象领域，以及每个DSL构造的抽象Transformers。然而，提出有用的抽象可能是不平凡的，因为它需要领域专业知识和关于合成器的知识。在本文中，我们提出了一种新的技术，用于学习抽象，是有用的实例化一个一般的合成框架在一个新的领域。给定一个DSL和一小部分训练问题，我们的方法使用树插值来推断可重用的谓词模板，从而加快给定域中的合成。我们的方法还学习合适的抽象Transformers，通过解决某种二阶约束求解问题的数据驱动的方式。我们在一个名为ATLAS的工具中实现了所提出的方法，并在BLAZE元合成器的背景下对其进行了评估。我们的评估表明，（a）ATLAS可以从很少的训练问题中学习有用的抽象域和Transformers，（b）与手工制作的抽象相比，ATLAS学习的抽象允许BLAZE实现更好的结果。
2018-04-11 cs.PL
Widening Operators for Weakly-Relational Numeric Abstractions (Extended Abstract)
我们讨论了最近发现的一些外推算子弱关系数值域的发散问题。我们确定的分歧的原因，并指出，诉诸更具体的，句法域可以避免通过研究合适的算法，消除冗余的限制，在所选择的表示。
2004-12-10 cs.PL
A DSL for Mapping Abstract Syntax Models to Concrete Syntax Models in ModelCC
ModelCC是一个基于模型的解析器生成器，它将语言设计与语言处理相结合。ModelCC提供了两种不同的机制来指定从抽象语法模型到具体语法模型的映射：在抽象语法模型规范之上定义的元数据注释和用于定义ASM-CSM映射的域特定语言。使用领域特定语言来指定从抽象语法模型到具体语法模型的映射允许为同一抽象语法模型定义多个具体语法模型。在本文中，我们描述了ModelCC域特定语言的抽象语法模型到具体的语法模型映射，我们展示了它的能力，提供了一个元定义的域特定语言。
2013-01-21 cs.PL
Non-Numerical Weakly Relational Domains
本文研究非数值弱关系域的构造，通过通用方法扩展常量传播并跟踪不等式合取，为格结构提供精确多项式算法，为NP完全情况提供抽象版本，并构造赋值和守卫的抽象转换器。
2024-01-10 cs.LO cs.PL
Synthesizing Abstract Transformers for Reduced-Product Domains
本文针对约减积域中抽象转换器合成搜索空间爆炸和组件协作困难的问题，提出基于多 DSL 的合成算法，并在工具 Amurth2 中实现，在 SAFEstr 框架的两个积域上取得了优于手工转换器的精度。
2024-08-07 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
Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics
本文提出在通用SemGuS框架下，利用语言语义的单调性属性，自动从具体语义获取基于区间的抽象语义以实现自动化剪枝，无需手动设计抽象域，有效提升了程序综合的搜索效率。
2024-08-28 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
Towards an Abstract Domain for Resource Analysis of Logic Programs Using Sized Types
提出了一种基于大小类型的逻辑程序通用资源分析方法，大小类型是一种包含结构（形状）信息的表示方法，它允许在任意位置和深度上表示一组项及其子项的大小的上下界.它们还允许在逻辑谓词中不同论元位置出现的术语和子术语的大小相关。使用这些大小的类型，资源分析可以推断的下限和上限的资源使用的程序中的所有程序作为输入项（和子项）的大小的函数，克服现有的分析和提高其精度的局限性。我们的新资源分析已经开发的抽象解释框架内，作为大小类型抽象域的扩展，并已集成到Ciao预处理器，CiaoPP。抽象域操作集成的递归方程的建立和求解，推断大小和资源使用功能。我们表明，该分析是一个改进，在CiaoPP目前的资源分析和比较以及功率的最先进的系统。
2013-08-19 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
Linear Dependent Types for Domain Specific Program Analysis (Extended Abstract)
在本教程中，我将介绍如何组合线性和依赖类型可以用来描述高阶程序的不同属性。线性类型已被证明对表达函数的属性特别有用;依赖类型对描述程序在控制流方面的行为很有用。这两个想法很好地结合在一起，当一个人有兴趣分析的功能取决于程序的控制流的属性。我将通过复杂性分析和敏感性分析的例子来说明这些想法。我将通过讨论这种方法的一般性来结束本教程。
2013-06-28 cs.PL
Making Abstract Domains Condensing
在本文中，我们表明，可逆分析的逻辑语言的抽象解释可以进行不损失的精度，系统地细化抽象域。其思想是将语义结构包含到抽象域中，以这种方式，精炼的抽象域变得足够丰富，以允许近似的自底向上和自顶向下语义一致。这些域被称为压缩抽象域。实质上，如果目标驱动和目标独立分析一致，则抽象域是浓缩的，即在目标独立分析中近似查询不会引起精度损失。我们证明了凝聚是一个抽象的域属性，并使一个抽象域凝聚的问题归结为问题，使域完整的统一。在一般的抽象解释设置，我们表明，当具体的域和操作引起quantales，即模型的命题线性逻辑，对象在一个完整的精炼抽象域可以明确的特征在于线性逻辑为基础的配方。这是用于逻辑程序分析的抽象域的情况，近似计算的答案替换，其中统一在幂等替换的Quantale中扮演乘法合取的角色。因此，凝聚抽象域可以通过最小限度地扩展任何，通常非凝聚域，由一个简单的域细化算子系统地得出。
2002-04-09 cs.LO cs.PL
Synthesizing Abstract Transformers
本文讨论了自动创建抽象Transformers的问题。我们提出的方法以类似于$\textit{yacc}$自动构造解析器的方式自动构造静态分析器。我们的方法对待的问题作为一个程序合成问题。用户提供（i）给定操作$\textit{op}$的具体语义，（ii）分析器要使用的抽象域A，以及（iii）域专用语言$L$的语义的规范，其中抽象Transformer要被表达。作为输出，我们的方法在抽象域A中为$\textit{op}$创建了一个抽象Transformer，用$L$表示（“A上的$\textit{op}$的$L$ -Transformer”）。此外，所获得的抽象Transformer是用于A上的$\textit{op}$的最精确的$L$ -Transformer;也就是说，不存在严格更精确的用于A上的$\textit{op}$的其他$L$ -Transformer。我们在一个名为AMURTH的工具中实现了我们的方法。我们使用AMURTH来创建用于两个现有分析仪的替换抽象Transformers，并获得了基本相同的性能。然而，当我们将现有的Transformers与使用AMURTH获得的Transformers进行比较时，我们发现现有的Transformers中有四个不可靠，这表明使用手动创建的Transformers存在风险。
2022-08-15 cs.PL
Domain Types: Selecting Abstractions Based on Variable Usage
软件模型检验的成功依赖于找到主题程序的适当抽象。抽象域和分析配置的选择目前留给用户，他们可能不熟悉可用抽象域的权衡和性能细节。我们引入域类型的概念，将程序变量分类为比标准声明类型（如int或long）更细粒度的类型，以指导模型检查器选择适当的抽象域。我们的实现在预处理步骤中确定每个变量的域类型，根据程序中的变量使用情况，然后将每个变量分配给一个抽象域。我们使用的模型检查框架支持为每个抽象域指定单独的分析精度，这样我们就可以自由地配置分析。我们的实验表明，每个变量的抽象域的选择的显着影响。我们考虑一个显式（整数值的哈希表）和一个符号（二元决策图）域。实验是基于标准的验证任务，从最近的软件验证比赛。每个抽象域在表示某个域类型的变量的状态空间方面具有独特的优势。我们的实验表明，软件模型检查器可以改善与域类型的指导组合的抽象域。
2013-05-28 cs.PL cs.SE
Quantified Data Automata on Skinny Trees: an Abstract Domain for Lists
我们提出了一种新的方法，堆分析通过一个抽象的自动机域，称为自动形状。抽象域使用一种特殊类型的自动机，称为瘦树上的量化数据自动机（QSDA），它允许定义单链表的通用量化属性。为了确保抽象不动点计算的收敛性，我们引入了一个称为弹性QSDA的QSDA子类，它也形成了一个抽象域。我们评估我们的方法在几个列表操作程序，我们表明，所提出的域是强大的，足以证明这些程序的一大类是正确的。
2013-04-02 cs.FL cs.PL
Abstract Interpretation of Binary Code with Memory Accesses using Polyhedra
在本文中，我们提出了一种新的方法，静态分析的二进制代码使用抽象解释。我们使用一个抽象域的基础上多面体和两个映射函数，关联多面体变量与寄存器和内存。我们证明了我们的方法来计算上限的问题，循环迭代的代码。这个问题在安全关键实时代码的最坏情况执行时间（WCET）分析领域尤为重要。然而，我们的方法是通用的，它可以适用于其他静态分析问题。
2017-11-20 cs.PL
Thread-modular Analysis of Release-Acquire Concurrency
我们提出了一个线程模块化的抽象解释（TMAI）技术来验证程序下的释放获取（RA）的内存模型的安全属性侵犯。我们的工作的主要贡献是：我们捕获的程序语句的执行顺序作为一个抽象的域，并提出了一个健全的上近似在这个域有效地原因RA并发。所提出的域在其应用中是通用的，并且捕获了作为抽象解释理论中的第一类特征的排序关系。特别地，域将并发程序中全局变量的修改序列的集合表示为偏序集合。在这种近似下，全局变量的较旧的sequenced-before存储被遗忘，并且仅保留每个变量的最新存储。我们建立我们提出的抽象的合理性，并在一个原型抽象解释器PRIORI中实现它们。PRIORI对现有的和具有挑战性的RA基准的评估表明，所提出的技术不仅在反驳方面具有竞争力，而且在验证方面也具有竞争力。与最近最先进的RA并发工具相比，PRIORI显示出更高的精度和更快的分析运行时间。
2021-08-17 cs.PL
Probabilistic Abstractions with Arbitrary Domains
Hermanns等人和Kattenbelt等人最近的工作已经将反例引导的抽象细化（CEGAR）扩展到概率程序。这些方法仅限于谓词抽象。我们提出了一种新的技术，基于Gulavani等人最近引入的抽象可达树，可以使用任意抽象域和加宽运算符（在抽象解释的意义上）。我们展示了如何合适的扩大运营商可以推导出循环不变量难以找到谓词抽象，并提出改进技术。
2011-06-16 cs.LO cs.PL
Abstract String Domain Defined with Word Equations as a Reduced Product (Extended Version)
提出一种基于字方程与不等式刻画字符串区间的抽象域，将其定义为字符串属性半格上的简化积，并证明其构成格，用于分析 JavaScript 字符串程序属性。
2025-10-13 cs.FL cs.PL
Synthesizing Best Abstract Transformers via Parallel Bit-Vector Optimization
The State Key Laboratory of Blockchain and Data Security, Zhejiang University（浙江大学区块链与数据安全国家重点实验室）；Shanghai Jiao Tong University（上海交通大学）
提出Spear并行合成框架，利用目标间位独立性加速最优抽象转换器合成，在二进制分析基准上优于现有OMT求解器。
2026-06-16 cs.PL
On the interaction between sharing and linearity
在逻辑程序的分析中，用于检测共享和线性信息的抽象域被广泛使用。设计这样的域的抽象统一算法已被证明是相当困难的。目前，可用的算法是正确的，但不是最佳的，即，它们不能充分利用由抽象域传达的信息。在本文中，我们定义了一个新的（无限）域ShLin-w，它可以被认为是一个一般的框架，其他域可以很容易地通过抽象得到。ShLin-w使共享和线性之间的相互作用变得明确。我们提供了一个建设性的表征的最佳抽象统一运营商的ShLin-w，我们提升到两个著名的抽象ShLin-w。即，经典的Sharing X Lin抽象域和Andy King的更精确的ShLin-2抽象域。在单绑定取代的情况下，我们得到最佳的抽象统一算法，这样的域。出现在逻辑编程理论与实践（TPLP）中。
2009-07-28 cs.LO cs.PL
Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains
异步消息传递系统经常用于实现分布式机制、协议和进程。本文针对这类系统的精确数据流分析问题。为了获得良好的精度，数据流分析需要以某种方式跳过读取的消息多于路径中迄今为止发送的消息数量的执行路径，因为这样的路径在运行时间是不可行的。现有的数据流分析技术确实省略了这样的不可行路径的子集，但它们具有仅允许有限的抽象分析域的限制。在本文中，我们提出了这些方法的推广，承认无限的抽象分析域，因为这些域通常用于在实践中获得高精度。我们已经实现了我们的方法，并分析了其性能的一组14个基准。在这些基准测试中，我们的工具获得了显着更高的精度相比，基线的方法，不省略任何不可行的路径和另一个基线，省略不可行的路径，但只承认有限的抽象域。
2021-01-25 cs.PL cs.SE
Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra
多面体形成了一个已建立的抽象域，用于使用抽象解释来推断程序的运行时属性。为了使整个静态分析结果可信，需要对它们的计算进行认证。在这项工作中，我们看看我们可以走多远的后验验证的道路，以降低多面体的抽象域的认证的开销。我们演示的方法，使包含证书生成的成本可以忽略不计。从性能的角度来看，我们的单一表示，基于约束的实现与最先进的实现相比。
2013-04-03 cs.LO cs.MS cs.PL
Decidability and Synthesis of Abstract Inductive Invariants
在许多软件和硬件验证系统中，在给定域范围内的归纳不变量的可判定性和综合起着重要的作用。我们认为在这里归纳不变量属于一个抽象域$A$的定义在抽象的解释，即，确保存在的最佳逼近$A$的任何系统属性。在这种情况下，我们研究的可判定性存在的抽象归纳不变量的$A$的过渡系统和相应的算法合成。我们的模型依赖于一些一般性的结果，这些结果将抽象归纳不变量的存在性与过渡系统的传递函数的$A$中的最佳正确逼近的最小不动点及其完备性联系起来。这种方法使我们能够推导出可判定性和合成结果的抽象归纳不变量，适用于著名的基尔达尔的常数传播和卡尔的仿射等式抽象域。此外，我们表明，最近的一般算法合成归纳不变量域的逻辑公式，可以系统地从我们的结果和推广到一系列的算法计算抽象归纳不变量。
2020-04-09 cs.LO cs.PL
Correctness Kernels of Abstract Interpretations
在基于抽象解释的静态分析中，近似是由抽象域编码的。它们为设计抽象语义函数提供了系统的指导，这些抽象语义函数近似于分析中的某些具体系统行为。为了近似给定的具体语义功能，抽象域可能包含冗余信息。本文介绍了抽象解释的正确性核的概念，一种简化抽象域的方法，即从它们中删除抽象值，以最大的方式，同时保留完全相同的近似行为的系统分析。我们表明，在抽象的模型检验正确性内核提供了一个由示例指导的抽象状态空间的简化范例，这意味着这种简化保留了示例的虚假性（即，抽象路径）。特别是，我们展示了如何正确的内核可以集成与著名的CEGAR（反例引导的抽象细化）方法。
2013-04-19 cs.LO cs.PL
A Constructive Framework for Galois Connections
基于抽象解释的静态分析依赖于程序属性的抽象域，例如整数变量的区间或全等。偏序集之间的伽罗瓦连接（GC）为数学上指定抽象域提供了最广泛和最有用的形式化工具。最近，Darais和Van Horn [2016]提出了无序集（而不是偏序集）的构造性伽罗瓦连接的概念，它允许以所谓的机械化和计算证明风格定义抽象域，因此可以使用Coq和Agda等证明助手自动提取静态分析的验证算法。我们在这里表明，建设性的GC是同构的，在一个精确和全面的意义，包括声音的抽象功能，所谓的分区GC-一个已知的类的GC，允许铸造标准集分区作为一个抽象域。Darais和Van Horn [2016]还为偏序集提供了构造性GC的概念，我们证明了它与普通GC同构，因此失去了它们的构造性属性。利用这些发现，我们提出并倡导使用纯粹的分区GC，一类新颖的建设性抽象域的机械化方法来抽象的解释。我们表明，这类抽象域使我们能够表示一组分区具有更大的灵活性，同时保留了建设性的方法伽罗瓦连接。
2017-04-28 cs.LO cs.PL
An Abstract Domain for Heap Commutativity (Extended Version)
本文提出一种面向堆操作程序的抽象域，将具体堆程序的交换性验证转移到抽象数学模型上安全执行，并支持框架化与组合推理，已在 Coq 中完成机械化。
2024-11-25 cs.LO cs.PL
A Decision Tree Lifted Domain for Analyzing Program Families with Numerical Features (Extended Version)
通过抽象解释的提升（基于族的）静态分析能够在一次运行中同时分析程序族的所有变体，而不显式地生成任何变体。底层提升分析域的元素是元组，每个变体维护一个属性。尽管如此，元组中的显式属性枚举（针对所有变体逐个）会立即产生组合爆炸。这是特别明显的情况下，程序的家庭，除了布尔功能，还包含数值功能与大域，从而承认天文配置空间。有效的提升分析的关键是正确处理语言的可变性特定结构（例如，基于功能的运行时测试和#if指令）。在这项工作中，我们引入了一个新的符号表示的提升抽象域，可以有效地分析程序族的数值特征。这使得与不同变体相对应的属性元素之间的共享显式地成为可能。新的提升域的元素是基于约束的决策树，其中决策节点被标记有在数值特征上定义的线性约束，并且叶节点属于现有的单个程序分析域。为了说明这种表示的潜力，我们实现了一个实验性的提升静态分析器，称为SPLNUM^2Analyzer，用于推断C程序的不变量。它使用现有的数值域（例如，间隔、八边形、多面体）作为参数。基于SV-COMP和BusyBox的基准测试结果表明，本文提出的基于决策树的方法是有效的，并且优于基于元组的方法，后者是基于抽象解释的基线提升分析。
2020-12-10 cs.LO cs.PL cs.SE
Abstractions of Sequences, Functions and Operators
针对递归函数闭式界推导难题，提出B-bound约束抽象域与域抽象函子，构建可处理高度非线性不变量的高阶抽象解释方法，适用于程序分析与混合系统等领域。
2025-07-30 cs.LO cs.PL
Computing Abstract Distances in Logic Programs
抽象解释是执行逻辑程序的静态分析的一种成熟的技术。然而，选择提供最佳精度-成本权衡的抽象域、加宽、固定点等仍然是一个悬而未决的问题。这在很大程度上是因为在测量和比较不同分析的精度方面存在挑战。我们提出了一种新的方法来测量这样的精度，定义在抽象域的距离，并将它们扩展到一个给定的程序的整个分析之间的距离，从而允许在不同的分析精度进行比较。我们调查和扩展现有的建议，在格或抽象域的距离和度量，我们提出了一些常见的域中使用的逻辑程序分析的度量，以及扩展这些度量的空间，整个程序分析。我们在CiaoPP框架内实现这些指标，并将它们应用于衡量基准和现实程序上不同分析的精度。
2019-07-30 cs.LO cs.PL
The Program Logic of Abstract Interpretation
Department of Mathematics, University of Padua（帕多瓦大学数学系）；Department of Computer Science, University of Pisa（比萨大学计算机系）
本文提出APPL逻辑，统一了Hoare逻辑、错误逻辑和超Hoare逻辑变体，提供抽象程序逻辑的理论基础，支持多种抽象域。
2026-11-09 cs.LO cs.PL
C Analyzer : A Static Program Analysis Tool for C Programs
INDIAN INSTITUTE OF TECHNOLOGY, BOMBAY（印度理工学院孟买分校）
本文提出C Analyzer，一个基于抽象解释技术的C程序静态分析工具，利用LLVM Clang API和CIL转换，支持多种抽象域以检测除零、溢出等运行时错误。
2024-01-28 cs.CL cs.PL
Hierarchical Shape Abstraction for Analysis of Free-List Memory Allocators
我们提出了一个分层的抽象域的分析自由列表内存分配器，跟踪形状和数值属性的堆和自由列表。我们的域是基于分离逻辑扩展的谓词，捕捉堆列表和自由列表的形状的指针算术约束。使用分层合成运算符组合这些谓词，以指定堆列表与自由列表的重叠。除了表现力之外，这个操作符还可以导致抽象值的组合和紧凑表示，并简化抽象域的实现。形状约束与整数数组上的数值约束相结合，以跟踪有关分配策略的属性（最佳拟合、首次拟合等）。这些属性超出了现有分析器的范围。我们实现了这个域，我们证明了它的有效性的几个实现的自由列表分配器。
2016-08-19 cs.LO cs.PL
A verified abstract machine for functional coroutines
函数式协程是一种受限形式的控制机制，其中每个协程都用延续和环境来表示。这个限制最初是通过考虑一个建设性的版本Parigot的经典自然演绎，这是健全的和完整的恒定域逻辑。在这篇文章中，我们提出了一个改进的de Groote的抽象机的功能协程，我们证明了它的正确性。因此，这个抽象机器也提供了常数域逻辑的直接计算解释。
2016-06-21 cs.LO cs.PL
An Experiment Combining Specialization with Abstract Interpretation
以前的研究表明，控制流细化可以通过一个程序专门化结合基于属性的抽象来实现，以提高终止和复杂性分析工具。我们现在表明，这个专门构建的专门化程序可以以更模块化的方式进行重构，并且可以使用现成的部分评估工具来实现先前的结果，并将其应用于抽象解释器。抽象解释器的关键特征是抽象域，它是基于属性的抽象域与具体域的乘积。这种独立于语言的框架提供了一种实用的方法来实现各种强大的专门化，并有助于使用解释器和专门化来实现程序转换的研究。
2020-08-07 cs.LO cs.PL cs.SC
Interval Slopes as Numerical Abstract Domain for Floating-Point Variables
提出一种基于区间斜率的部分关系抽象域，用于浮点变量的静态分析，能够模拟浮点算术行为，验证嵌入式控制系统中的运行时错误和数值精度。
2010-06-18 cs.NA cs.PL math.NA
Using Ellipsoidal Domains to Analyze Control Systems Software
我们提出了一种基于动态系统的控制器安全性能自动验证的方法，例如通常用于航空电子设备的控制器。特别是，我们的重点是证明软件实现线性和一些非线性控制器的稳定性。我们开发了一个抽象的解释框架，紧接着在模型级的证明中使用的李雅普诺夫方法，并描述相应的抽象域，其中线性系统的椭球约束。这些椭圆域提供了状态变量值的抽象，并且必须与对程序中的其余变量进行建模的其他域相结合。因此，自动为每个变量分配正确类型的抽象域的问题出现了。我们提供了一个算法，解决了这个分类问题，在许多实际情况下，并建议如何将其推广到更复杂的情况。然后，我们通过求解矩阵方程找到一个不动点，在线性情况下，这只是离散的李雅普诺夫方程。与软件分析中的大多数情况相反，这个不动点不能通过通常的传播约束的迭代法达到饱和，因此数值方法变得必不可少。最后，我们用几个例子来说明我们的方法。
2009-09-10 cs.PL cs.SE
Automatic Repair of Overflowing Expressions with Abstract Interpretation
我们考虑合成可证明非溢出整数算术表达式或整数算术表达式之间的布尔关系的问题。首先，我们使用一个数值抽象域来推断程序变量之间的数值属性。然后我们检查这些属性是否保证给定的表达式不会溢出。如果不是这种情况，我们合成一个等价的，但不溢出的表达式，或者我们报告这样的表达式不存在。非溢出表达式的合成取决于三个正交因素：输入表达式（例如，是线性的，多项式的，?),输出表达式（例如，是否允许进行情况拆分？），和底层的数值抽象域--抽象域越精确，就能合成越正确的表达式。我们考虑三种常见的情况：（i）整数系数和区间的线性表达式;（ii）线性表达式的布尔表达式;和（iii）线性表达式与模板。在第一种情况下，我们证明了存在一个完整的多项式算法来解决这个问题。在第二种情况下，我们有一个不完整的多项式算法，而在第三种情况下，我们有一个完整的，但最坏情况的指数算法。
2013-09-20 cs.PL cs.SE
Structured general corecursion and coinductive graphs [extended abstract]
Bove和Capretta用一般递归方程来证明函数定义的流行方法是基于这样的观察：任何结构化的一般递归方程定义了一个预期域（“定义域”）的归纳子集，该方程具有唯一的解。要接受这个定义，只要证明这个子集包含整个预定域就足够了。这种方法对于“终止”定义非常有效。但是它没有考虑到“生产性”的定义，例如流值函数的典型定义。我们认为，这样的定义可以被视为在一个类似的精神，从一个不同的独特的可解性标准。任何结构化的递归方程都定义了预定域和预定余域之间的共归纳关系（“共归纳图”）。这个关系又确定了一个子集的预期域和商的预期的余域的属性，该方程是唯一解决的子集和商。因此，只要子集是全集且商是相等的，就保证方程对于预定域和预定余域有唯一解。
2012-02-16 cs.LO cs.PL
Refining Existential Properties in Separation Logic Analyses
在分离逻辑程序分析中，易处理性通常通过将不变量限制在有限的抽象域来实现。由于这个域不能变化，即使在底层逻辑中可以进行验证，信息丢失也可能导致失败。在本文中，我们提出了一种类似CEGAR的方法，用于检测虚假故障并通过细化抽象域来避免它们。我们的方法是面向发现存在的属性，例如“列表包含值x”。为了诊断故障，我们使用溯因推理，这是一种用于推断命令先决条件的技术。我们的方法从错误向后工作，识别因抽象而丢失的必要信息，并改进正向分析以避免错误。我们定义了几类存在属性的域，并在Redis，Azureus和FreeRTOS的案例研究中展示了它们的有效性。
2015-04-30 cs.LO cs.PL
A Technology for BigData Analysis Task Description using Domain-Specific Languages
本文提出了一种基于知识的领域特定语言（DSL）动态构建技术，用于使用大数据技术描述数据密集型科学发现任务。所提出的技术支持任务的分析和模拟部分的高级抽象定义，以及集成到复合科学解决方案中。抽象任务定义的自动转换使单个解决方案中的各种数据源能够实现无缝集成。
2014-04-18 cs.DB cs.DC cs.PL
