Abstract Interpretation as a Programming Language
在David Schmidt的博士论文中，他探索了指称语义作为程序设计语言的使用。这是一项努力的一部分，不仅将形式语义视为规范，而且还将其视为编译器生成器的解释器和输入。语义本身可以被看作是一个程序，人们可以检查不同的编程风格和表示状态的方法。抽象解释主要是一种用于推导和规范程序分析的技术。与指称语义一样，我们也可以将抽象解释视为程序并检查其实现。本文的主要重点是表明，高阶严格性分析的结果可以更普遍地用作格上高阶函数的不动点算子，从而提供了一种立即实现一大类抽象解释的技术。此外，它可以被视为一种编程范式，并用于以循环风格编写程序。
2013-09-20 cs.PL
Extended abstract: Type oriented programming for task based parallelism
编写并行代码是困难的，并且在抽象和性能之间表现出基本的权衡。设计用于简化并行性复杂性的高级语言抽象做出了某些影响性能和可伸缩性的假设。另一方面，低级语言提供了许多优化的机会，需要深入的知识和程序员考虑并行性的棘手细节。需要一种方法，可以弥合差距，并提供编程的便利性和控制和优化的机会。通过可选地用附加的类型信息装饰代码，程序员可以指导编译器做出某些决定，或者依赖于合理的默认选择。
2020-10-27 cs.PL
Lost in Abstraction: Monotonicity in Multi-Threaded Programs (Extended Technical Report)
并发系统中的单调性规定，在任何全局状态下，当新进程添加到该状态时，现存的系统操作仍然是可执行的。这个概念在多线程软件中不仅是自然和常见的，而且很有用：如果每个线程的内存是有限的，单调性通常保证安全属性验证的可判定性，即使在运行线程的数量未知的情况下。在本文中，我们表明，获得有限数据线程抽象的模型检验的行为可能与单调性不一致：谓词抽象某些广泛使用的单调软件的结果在非单调的多线程布尔程序的单调性是失去了抽象。其结果是，完善的健全和完整的安全检查算法变得不适用，事实上，安全检查原来是不可判定的无界线程布尔程序类。我们演示了如何将抽象程序修改为单调程序，而不影响非单调抽象的安全属性。这显着改进了早期通过过度逼近来强制单调性的方法。
2014-06-24 cs.PL
On Propositional Program Equivalence (extended abstract)
本文从带保护的Kleene代数与测试的视角，讨论命题程序等价性的最新进展，该等价性在抽象语句语义后可判定且实践可行。
2025-07-10 cs.PL
Automating Abstract Interpretation of Abstract Machines
静态程序分析对于人们编写程序所使用的任何程序设计语言来说都是一种有价值的工具。脚本语言在世界上的流行表明，程序设计语言解释器相对容易编写。这些语言的用户抱怨他们没有能力分析他们的代码，因此程序设计语言分析器并不容易编写。本文研究了一种从传统解释器生成抽象解释器的系统方法，称为抽象抽象机。由于技术、理论和语用问题，抽象口译员很难发展。技术问题包括工程数据结构和算法。我表明，适度和简单的变化，抽象机器的数学表示的结果，在1000倍更好的运行时间-只是几秒钟的中等大小的程序。在理论领域，抽象会使正确性难以确定。我提供了证明技术，通过将计算能力留给外部因素：分配来证明抽象计算的常规、下推和堆栈检查下推模型的正确性。即使我们不信任证明，我们也可以针对测试套件具体地运行模型，以更好地信任它们。在务实的领域，我表明，抽象的抽象机器的系统过程是自动化的。我开发了一种类似于其他语义工程语言的用于表达抽象机器的元语言。该语言的特殊之处在于它提供了一个抽象分配的接口。语义保证，如果分配是有限的，那么语义是一个可靠的和可计算的近似的具体语义。
2015-04-29 cs.PL
Abstracting Abstract Machines: A Systematic Approach to Higher-Order Program Analysis
预测模型是设计可靠软件系统的基础。然而，对于现代高级程序设计语言来说，为程序的行为（静态分析）设计保守的、可计算的近似值仍然是一个困难且容易出错的过程。分析设计师需要的是一种原则性的方法，用于在语义和分析模型之间导航：分析设计师需要一种方法，可以驯服复杂语言功能的交互，例如高阶函数，递归，异常，延续，对象和动态分配。我们贡献了一个系统的方法程序分析，产生新颖的和透明的声音静态分析。我们的方法依赖于现有的派生技术，将高级语言语义转换为低级别的确定性状态转换系统（具有潜在的无限状态空间）。然后，我们进行了一系列简单的机器重构，以获得一个声音，可计算的近似，它采取的形式与有限的状态空间的非确定性状态转换系统。该方法统一地扩展到支持对实际语言特性的程序分析，包括高阶函数、尾调用、条件、副作用、异常、第一类延续，甚至垃圾回收。
2011-05-09 cs.PL
C++ programming language for an abstract massively parallel SIMD architecture
这项工作的目的是定义和实现一个扩展的C++语言，以支持SIMD编程范式。C++程序设计语言已被扩展以表达由中央控制处理器和N维环形数字处理器阵列组成的抽象SIMD机的所有潜力。很少有扩展被添加到标准C++中，目的是最大限度地减少程序员学习新语言的努力，并保持编译代码的高性能。所提出的语言已实现为一个移植的GNU C++编译器上的SIMD超级计算机。
2000-05-19 cs.PL
Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics
本文提出在通用SemGuS框架下，利用语言语义的单调性属性，自动从具体语义获取基于区间的抽象语义以实现自动化剪枝，无需手动设计抽象域，有效提升了程序综合的搜索效率。
2024-08-28 cs.PL
Learning Abstractions for Program Synthesis
许多示例引导的程序合成技术使用抽象来修剪搜索空间。虽然基于抽象的合成已经被证明是非常强大的，但领域专家需要提供一个合适的抽象领域，以及每个DSL构造的抽象Transformers。然而，提出有用的抽象可能是不平凡的，因为它需要领域专业知识和关于合成器的知识。在本文中，我们提出了一种新的技术，用于学习抽象，是有用的实例化一个一般的合成框架在一个新的领域。给定一个DSL和一小部分训练问题，我们的方法使用树插值来推断可重用的谓词模板，从而加快给定域中的合成。我们的方法还学习合适的抽象Transformers，通过解决某种二阶约束求解问题的数据驱动的方式。我们在一个名为ATLAS的工具中实现了所提出的方法，并在BLAZE元合成器的背景下对其进行了评估。我们的评估表明，（a）ATLAS可以从很少的训练问题中学习有用的抽象域和Transformers，（b）与手工制作的抽象相比，ATLAS学习的抽象允许BLAZE实现更好的结果。
2018-04-11 cs.PL
Abstract Program Slicing: an Abstract Interpretation-based approach to Program Slicing
在本文中，我们正式定义了抽象程序切片的概念，程序切片的一般形式被认为是数据的属性，而不是它们的确切值。这种方法适用于具有数值和引用值的语言，并依赖于程序组件（语句）之间的抽象依赖关系的概念。不同形式的（后向）抽象切片被添加到现有的正式框架中，传统的非抽象形式的切片可以进行比较。扩展的框架使我们能够理解抽象切片是传统切片的推广，因为传统切片（处理语法依赖关系）是由（语义）非抽象形式的切片推广的，这实际上相当于对数据执行身份抽象的抽象形式。声音算法计算抽象的依赖关系和程序片的系统表征，它依赖于程序状态之间的协议的概念。
2016-05-17 cs.LO cs.PL
Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics
University of Michigan（密歇根大学）；University of Texas at Austin（德克萨斯大学奥斯汀分校）
本文提出Presynthesis方法，通过引入离线预合成阶段，利用树自动机和oracle提升程序合成效率，显著优于现有方法。
2026-04-16 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
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 anti-refinement
本文展示了命令式程序的抽象解释和精化演算之间的对应关系：在精化演算中，程序的抽象解释是一个规范，它是一个函数。这种对应关系可以用来指导设计机械验证的静态分析，保持正确性证明以及分离的启发式部分的算法。
2014-06-13 cs.PL
Optimal Program Synthesis via Abstract Interpretation
University of Pennsylvania（宾夕法尼亚大学）
本文提出了一种基于抽象解释的框架，用于在领域特定语言中高效合成最优程序，通过A*搜索和抽象转换器提升可扩展性。
2026-02-16 cs.PL
Structural Resolution for Abstract Compilation of Object-Oriented Languages
我们提出了基于共归纳逻辑编程的面向对象语言的精确静态类型分析的抽象编译。源代码被翻译成一个逻辑程序，然后类型检查和推理问题就变成了要解决的关于结果逻辑程序的查询。我们利用共归纳语义来处理递归类型和方法产生的无限项和证明。由于最近的概念，结构解析共归纳逻辑编程，我们能够推断出非常精确的类型信息，包括一类不合理的递归类型，导致非终止先前考虑共归纳语义。我们还展示了如何转换逻辑程序，使它们满足结构归结的操作语义的先决条件，我们证明了这一步骤不影响的语义的逻辑程序。
2017-09-14 cs.PL
Towards an Abstract Domain for Resource Analysis of Logic Programs Using Sized Types
提出了一种基于大小类型的逻辑程序通用资源分析方法，大小类型是一种包含结构（形状）信息的表示方法，它允许在任意位置和深度上表示一组项及其子项的大小的上下界.它们还允许在逻辑谓词中不同论元位置出现的术语和子术语的大小相关。使用这些大小的类型，资源分析可以推断的下限和上限的资源使用的程序中的所有程序作为输入项（和子项）的大小的函数，克服现有的分析和提高其精度的局限性。我们的新资源分析已经开发的抽象解释框架内，作为大小类型抽象域的扩展，并已集成到Ciao预处理器，CiaoPP。抽象域操作集成的递归方程的建立和求解，推断大小和资源使用功能。我们表明，该分析是一个改进，在CiaoPP目前的资源分析和比较以及功率的最先进的系统。
2013-08-19 cs.PL
A simple abstraction of arrays and maps by program translation
我们提出了一种处理数组的程序的静态分析方法，数组程序的语义和纯标量操作的语义之间有伽罗瓦连接。实现它的最简单的方法是通过自动地将数组程序语法转换为标量程序，然后使用任何静态分析技术（抽象解释、加速、谓词抽象等）分析标量程序。.).由此获得的标量不变量被翻译回原始程序作为普遍量化的数组不变量。我们说明了我们的方法上的各种例子，导致“荷兰旗”算法。
2015-06-12 cs.LO cs.PL
Interactive Abstract Interpretation: Reanalyzing Whole Programs for Cheap
为了使静态程序分析在软件开发人员的指尖，我们提出了一个框架的交互式抽象解释。虽然提供了合理的分析结果，但抽象解释通常可能非常昂贵。为了实现快速的响应时间，我们增加了分析基础设施，包括后处理，而不需要对分析规范本身进行任何修改。我们依赖于本地通用定点引擎TD，它动态跟踪依赖关系，同时探索有助于回答初始查询的未知数。对受程序变化影响的分析结果采用惰性失效方法。专门的改进支持并发缺陷（如数据竞争）的增量分析。该框架已在静态分析器Goblint中为多线程C实现，使用MagpieBridge将发现中继到IDE。我们评估我们的实施w.r.t.响应时间和一致性的标尺：以前证明的不变量应该被保留-当它们不受变化的影响时。结果表明，与我们的方法，小的变化后的重新分析只需要一小部分的从头开始的分析时间，而大部分的精度被保留。我们还提供了程序开发的例子，突出了整体方法的可用性。
2022-11-25 cs.PL
Delay-Bounded Scheduling Without Delay! (Extended Technical Report)
我们认为，在任意线程交织的异步并发程序的安全性分析的广泛问题。延迟有界的确定性调度，介绍了在以前的工作中，是一个有效的错误发现技术，以遏制与充分的调度不确定性的大成本。在本文中，我们首先提出了一种技术，以解除有限域变量程序的情况下的延迟界，从而增加了效率的错误检测的能力，证明安全的程序在任意线程交织。其次，我们展示了如何，结合谓词抽象，我们的技术可以反驳和验证安全属性的程序与无界的变量域，即使是无限的线程数。以前的工作已经建立，对于非平凡的并发例程，谓词抽象诱导一个高度复杂的抽象程序语义。然而，我们的技术，从来没有静态地构造一个抽象的参数化程序，它只需要一些抽象状态集在某些行动下被关闭，从而消除了对存在的抽象程序的验证算法的依赖。我们证明了我们的技术在以前的工作中使用的许多例子的效率，并展示其简单性相比，早期的方法在无限线程票锁协议。
2021-05-15 cs.PL
Deriving Abstract Semantics for Forward Analysis of Normal Logic Programs
虽然否定作为失败是通过内建谓词来处理的，但在文献中还没有正式地讨论{ \em normal}逻辑程序的前向抽象解释问题！在Prolog中实现的方式。本文提出了一个解决这个问题的方法，推导出两个通用的不动点抽象语义$F^b and $ F^ \diamond { \em正常}逻辑程序的前向抽象解释。$F^b$用于推断程序图中边的数据描述，其中边表示执行控制从其源程序点转移到其目的程序点的可能性。$F^\diamond$源自$F^b$，用于推断文本程序点的数据描述。
1998-11-06 cs.LO cs.PL
Abstracting Runtime Heaps for Program Understanding
现代编程环境提供了广泛的支持，检查，分析和测试程序的基础上的算法结构的程序。不幸的是，对在执行期间检查和理解运行时数据结构的支持通常受到更多限制。本文提供了一种通用的技术来抽象和总结整个运行时堆。我们描述了抽象堆模型和相关的算法，用于将具体堆转储转换为相应的抽象模型，以及用于合并，比较和计算抽象模型之间的变化的算法。抽象模型旨在强调有关基于堆的数据结构的高级概念，如形状和大小，以及堆结构之间的关系，如共享和连接。我们通过构建一个内存分析器来展示抽象堆模型的实用性和计算易处理性。然后，我们使用这个工具来检查，查明和纠正来自DaCapo的一套程序的内存膨胀的来源。
2012-01-06 cs.PL cs.SE
An Abstract Monte-Carlo Method for the Analysis of Probabilistic Programs
本文介绍了一种新的方法，随机测试和抽象解释相结合，用于分析具有概率和非概率不确定性的程序。在介绍了“普通”测试后，我们展示了如何将测试和抽象解释相结合，并给出了将结果的精度与迭代次数联系起来的公式。然后，我们讨论了复杂性和优化问题，并结束了一些实验结果。
2007-01-30 cs.PF cs.PL
HMC: Verifying Functional Programs Using Abstract Interpreters
我们提出了Hindley-Milner-Cousots（HMC），一个算法，允许任何一阶命令式程序的过程间分析被用来验证类型化高阶函数程序的安全属性。HMC工作如下。首先，它利用函数程序的类型结构来生成一组逻辑精化约束，这些约束的满足意味着源程序的安全性。其次，它将逻辑精化约束转换成一个简单的一阶命令式程序，该程序是安全的，当且仅当约束是可满足的。因此，HMC一举使工具的不变生成，例如，基于抽象域、谓词抽象、反例引导的精化和Craig插值可以直接应用于以全自动的方式验证现代函数式语言的安全属性。我们已经实现了HMC，并描述了初步的实验结果，使用两个命令式检查器- ARMC和InterProc -来验证OCaml程序。因此，通过组成基于类型的推理在程序语法和基于状态的推理在抽象解释的基础上，HMC打开了大门，以现代程序设计语言编写的程序的自动验证。
2010-12-30 cs.LO cs.PL
Computing Abstract Distances in Logic Programs
抽象解释是执行逻辑程序的静态分析的一种成熟的技术。然而，选择提供最佳精度-成本权衡的抽象域、加宽、固定点等仍然是一个悬而未决的问题。这在很大程度上是因为在测量和比较不同分析的精度方面存在挑战。我们提出了一种新的方法来测量这样的精度，定义在抽象域的距离，并将它们扩展到一个给定的程序的整个分析之间的距离，从而允许在不同的分析精度进行比较。我们调查和扩展现有的建议，在格或抽象域的距离和度量，我们提出了一些常见的域中使用的逻辑程序分析的度量，以及扩展这些度量的空间，整个程序分析。我们在CiaoPP框架内实现这些指标，并将它们应用于衡量基准和现实程序上不同分析的精度。
2019-07-30 cs.LO cs.PL
Collecting Graphical Abstract Views of Mercury Program Executions
程序执行监视器是收集和抽象有关程序执行的信息的程序。“collect”操作符是一个高级的通用原语，它允许用户实现自己的监视器。“收集”建立在水星轨迹之上。在以前的工作中，我们已经演示了如何使用该操作符来有效地收集有关Mercury程序执行的各种统计信息。在本文中，我们通过提供更多的监视器示例，进一步展示了“collect”的表达能力和有效性。特别是，我们将展示如何实现监视器，生成图形抽象的程序执行，如证明树，控制流图和动态调用图。我们展示了这些抽象如何可以很容易地修改和适应，因为这些监视器只需要几十行代码。这些抽象旨在作为软件可视化工具的前端。虽然“collect”目前是在Mercury跟踪之上实现的，但它的基本概念都不依赖于Mercury，它可以在任何程序设计语言的任何跟踪程序之上实现。
2000-10-31 cs.PL cs.SE
Automatic Probabilistic Program Verification through Random Variable Abstraction
最弱预期望演算已被证明是分析概率和不确定性规划定量性质的成熟理论。我们提出了一个自动的方法证明定量线性性质的任何可数状态空间使用迭代向后不动点计算的一般框架中的抽象解释。为了完成这一任务，我们提出了随机变量抽象（RVA）的技术，我们还假设了一个充分条件，实现精确的不动点计算的抽象域。我们的方法的可行性示出了两个例子，一个获得的概率程序的预期运行时间，和其他的赌博策略的预期收益。我们的方法适用于一般的保护概率和不确定性的过渡系统，而不是普通的pGCL程序，使我们能够很容易地模拟广泛的系统，包括分布式的和非结构化的程序。我们提出了该程序的操作和最弱前提语义，并证明了它的等价性。
2010-06-26 cs.LO cs.PL
TWAM: A Certifying Abstract Machine for Logic Programs
类型保持（或类型化）编译使用类型化派生来证明编译的正确性。我们为Prolog的简单类型方言设计并实现了一个类型保留编译器，我们称之为T-Prolog。我们的方法的关键是一个新的认证抽象机，我们称之为类型沃伦抽象机（TWAM）。TWAM有一个足够强的依赖类型系统来指定逻辑框架LF中的逻辑程序的语义。我们提出了一个合理性元定理，它构成了部分正确性保证：良好类型的程序实现的逻辑程序指定的类型。这个元定理证明了我们的设计和实现的证明编译器从T-Prolog到TWAM。
2018-01-01 cs.LO cs.PL
A Program Logic for Abstract (Hyper)Properties
Department of Mathematics, University of Padua（帕多瓦大学数学系）；Department of Computer Science, University of Pisa（比萨大学计算机系）
本文提出APPL逻辑，统一了Hoare逻辑、错误逻辑和超Hoare逻辑变体，提供抽象程序逻辑的理论基础，支持多种抽象域。
2026-04-21 cs.LO cs.PL
Automatic Modular Abstractions for Linear Constraints
提出了一种通过抽象解释自动生成用于静态分析的抽象Transformers的方法。该方法的重点是对程序的线性约束，操作合理的，真正的或浮点变量，并包含线性分配和测试。除了无循环代码，同样的方法也适用于获得最小不动点作为前提条件的函数，这允许分析循环和递归函数。我们的算法是基于新的量词消去和符号操作技术。给定一个抽象域的规范和一个程序块，我们的方法自动输出相应的抽象Transformer的实现。因此，它是程序转换的一种形式。我们工作的动机是数据流同步程序设计语言，用于构建控制命令嵌入式系统，但它也适用于命令式和函数式编程。
2008-11-02 cs.LO cs.PL
Automatic modular abstractions for template numerical constraints
提出了一种通过抽象解释自动生成用于静态分析的抽象Transformers的方法。该方法的重点是对程序的线性约束，操作合理的，真正的或浮点变量，并包含线性分配和测试。除了无循环代码，同样的方法也适用于获得最小不动点作为前提条件的函数，这允许分析循环和递归函数。我们的算法是基于新的量词消去和符号操作技术。给定一个抽象域的规范和一个程序块，我们的方法自动输出相应的抽象Transformer的实现。因此，它是程序转换的一种形式。我们工作的动机是数据流同步程序设计语言，用于构建控制命令嵌入式系统，但它也适用于命令式和函数式编程。
2010-05-31 cs.LO cs.PL
Extended Abstract: Mutable Objects with Several Implementations
本研究介绍ACL2 8.6版本新增的attach-stobj特性，该特性支持为抽象stobj配置不同可执行操作且无需重新认证相关书籍与定理，同时给出了背景、用户概述及实现说明。
2025-07-25 cs.LO cs.PL
Automatic Modular Abstractions for Template Numerical Constraints
提出了一种通过抽象解释自动生成用于静态分析的抽象Transformers的方法。该方法的重点是对程序的线性约束，操作合理的，真正的或浮点变量，并包含线性分配和测试。给定一个抽象域的规范和一个程序块，我们的方法自动输出相应的抽象Transformer的实现。因此，它是程序转换的一种形式。除了无循环代码，同样的方法也适用于获得最小不动点作为前提条件的函数，这允许分析循环和递归函数。我们工作的动机是数据流同步程序设计语言，用于构建控制命令嵌入式系统，但它也适用于命令式和函数式编程。我们的算法是基于线性算术公式上的量词消去和符号操作技术。我们也给出了非线性约束和非线性程序结构的一般结果。
2010-05-26 cs.LO cs.PL
Abstract Diagnosis for Timed Concurrent Constraint programs
时间并发约束语言（Timed Concurrent Constraint Language，简称tccp）是一种基于简单但功能强大的并发约束范式Saraswat的并发逻辑语言。在这种范例中，存储作为值的概念被存储作为约束的概念所取代，这引入了与存储作为值的概念的一些差异。其他并发方法。在本文中，我们提供了一个通用的框架调试tccp程序。为此，我们首先提出了一个新的紧凑的，自底向上的语义的语言，非常适合于调试和验证的目的，在反应式系统的上下文中。我们还提供了一个抽象的语义，使我们能够有效地实现基于抽象解释的调试算法。给定一个tccp程序和一个行为规范，我们的调试方法自动检测程序是否满足规范。这与其他半自动调试方法不同，避免了提前提供症状的需要。我们通过介绍两个说明性的例子来展示我们的方法的有效性。我们选择一个特定的抽象域，并展示我们如何可以检测到一个程序是错误的。
2011-09-07 cs.LO cs.PL
AbstractBeam: Enhancing Bottom-Up Program Synthesis using Library Learning
University of Mannheim（曼海姆大学）
针对现有程序合成算法LambdaBeam未利用重复程序结构的问题，提出集成库学习的AbstractBeam框架，将重复结构融入DSL，在整数列表操作领域显著提升合成效果与效率，拓展了库学习的适用范围。
2024-09-12 cs.AI cs.PL cs.SE
Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers (Extended Manuscript)
我们解决的问题，分析异步事件驱动的程序，并发代理通过无界消息队列进行通信。这类程序的安全验证问题是不可判定的。在本文中，我们提出了一种技术，结合了有界探索的收敛性测试：如果序列的某些抽象的可达状态，增加队列界限k，收敛，我们可以证明任何属性的程序，是由抽象保存。如果抽象状态空间是有限的，则收敛是有保证的;挑战在于捕捉它发生的点k_max。我们进一步证明了如何简单的不变量制定的具体域可以用来消除虚假的抽象状态，否则会阻止序列收敛。我们已经实现了我们的技术的P程序设计语言的事件驱动程序。我们的实验表明，序列的抽象往往完全自动收敛，在困难的情况下，最小的设计师支持的形式顺序可证明的不变量，这发生在一个值的k_max足够小，让该方法在实践中取得成功。
2019-05-24 cs.FL cs.LO cs.PL
Abstract Compilation as Abstraction of Operator Semantics, applied to Cost Analysis
Universidad Politécnica de Madrid（马德里理工大学）；IMDEA Software Institute（IMDEA软件研究所）；Spanish Council for Scientific Research (CSIC)（西班牙国家研究委员会）；Computer Science Laboratory of Sorbonne University (LIP6)（索邦大学计算机科学实验室）；STMicroelectronics（意法半导体）
该研究提出算子语义与抽象编译框架，将其应用于静态代价分析，开发出支持通用函数未知量等的最优递归提取技术，提升了代价分析的可靠性与精确性。
2026-08-11 cs.LO cs.PL
An Abstract Domain for Heap Commutativity (Extended Version)
本文提出一种面向堆操作程序的抽象域，将具体堆程序的交换性验证转移到抽象数学模型上安全执行，并支持框架化与组合推理，已在 Coq 中完成机械化。
2024-11-25 cs.LO cs.PL
A Prolog-based Environment for Reasoning about Programming Languages (Extended abstract)
ECLAIR是一个基于Prolog的原型系统，旨在为程序设计语言分析和实现工具的研究、开发和评估提供一个功能完整的环境。在本文中，我们勾画了系统的总体结构，概述了其组件的主要方法和技术。我们还讨论了Prolog作为系统实现语言的适当性：除了突出其优点外，我们还指出了一些潜在的弱点，暗示了可能的解决方案。
2007-11-02 cs.PL cs.SE
Constraint-based verification of abstract models of multitreaded programs
我们提出了一种多线程程序的抽象模型的自动验证技术，提供新鲜的名称生成，名称移动性和无界控制。作为高级规约语言，我们在这里采用了一个扩展的通信有限状态机的局部变量范围在一个无限的域名，称为TDL程序。通信机已被证明是非常有效的表示通信协议，以及表示多线程软件的抽象。我们提出的验证方法是基于编码的TDL程序成一个低级语言的基础上多集重写和约束，可以被看作是一个扩展的Petri网。通过这种编码，符号验证过程中开发的低级语言在我们以前的工作，现在可以应用到TDL程序。此外，编码使我们能够隔离TDL程序，仍然提供新鲜的名称生成，名称移动性和无界控制的可判定类的验证问题。我们的语法限制实际上是在线程的内部结构上定义的：为了获得一个完整的终止方法，线程最多只能有一个局部变量（范围在无限的域名上）。
2006-01-10 cs.CL 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
Constraint-based automatic verification of abstract models of multithreaded programs
我们提出了一种多线程程序的抽象模型的自动验证技术，提供新鲜的名称生成，名称移动性和无界控制。作为高级规约语言，我们在这里采用了一个扩展的通信有限状态机的局部变量范围在一个无限的域名，称为TDL程序。通信机已被证明是非常有效的表示通信协议，以及表示多线程软件的抽象。我们提出的验证方法是基于编码的TDL程序成一个低级语言的基础上多集重写和约束，可以被看作是一个扩展的Petri网。通过这种编码，符号验证过程中开发的低级语言在我们以前的工作，现在可以应用到TDL程序。此外，编码使我们能够隔离TDL程序，仍然提供新鲜的名称生成，名称移动性和无界控制的可判定类的验证问题。我们的语法限制实际上是在线程的内部结构上定义的：为了获得一个完整的终止方法，线程最多只能有一个局部变量（范围在无限的域名上）。
2006-01-10 cs.LO cs.PL
Parameterized Dataflow (Extended Abstract)
数据流网络应用于各种形式的流处理，例如用于多媒体数据的并行处理。图的描述，包括他们的点火行为，通常是非组合的，不适合单独编译。这篇文章考虑了一种带有类型和效果系统的Repllow语言，该系统捕获了演员的触发行为。该系统允许定义抽象化Actor触发率，支持Actor定义的定义和安全组合，其中触发率直到启动Cowllow图才被实例化。
2016-10-26 cs.DC cs.PL
Abstract String Domain Defined with Word Equations as a Reduced Product (Extended Version)
提出一种基于字方程与不等式刻画字符串区间的抽象域，将其定义为字符串属性半格上的简化积，并证明其构成格，用于分析 JavaScript 字符串程序属性。
2025-10-13 cs.FL cs.PL
Convergence in Infinitary Term Graph Rewriting Systems is Simple (Extended Abstract)
在这个扩展的摘要中，我们提出了一个简单的方法来收敛项图，使我们能够统一项图重写和无穷项重写。这种方法是基于偏序和度量的术语图。这些结构是无穷项重写中使用的相应结构的简单概括。我们将我们的简单方法与我们之前开发的更复杂的方法进行比较，并表明这种新方法在许多方面都更优越。唯一不利的财产，我们能够确定，即失败的弱度量和偏序收敛之间的充分对应，是通过采用强收敛纪律纠正。
2013-02-26 cs.LO cs.PL
Verifying C11-Style Weak Memory Libraries
演绎验证的并发程序在弱内存下，到目前为止，仅限于简单的程序在一个单一的状态空间。对于可伸缩性，我们还需要具有可验证库抽象的模块化技术。本文解决了这一挑战的背景下，RC 11 RAR，C11内存模型的一个子集，允许放松和释放获取访问，但不允许，所谓的负载缓冲周期。我们开发了一个简单的框架，用于指定抽象对象，精确地描述了抽象方法调用的可观察性保证。我们展示了如何将这个框架与一个操作语义集成，该操作语义使客户端程序执行它使用的库中的抽象方法调用的验证成为可能。最后，我们将展示如何实现这样的抽象在RC 11 RAR可以验证通过开发一个（上下文）细化框架的抽象对象。我们的框架，包括操作语义，客户端库程序的验证技术，和抽象库和它们的实现之间的模拟，已在伊莎贝尔/HOL机械化。
2020-12-28 cs.LO cs.PL
LLMs program using Reusable and Composable Abstract Representations
Simplex；MATS Astera Institute（MATS Astera研究所）；Astera Institute（Astera研究所）；University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）
该研究发现LLMs生成代码时会形成可复用可组合的抽象表示，可独立操控函数、语言等要素，跨语言泛化能力强，合成数据训练的Transformer也能学习此类表示。
2026-10-13 cs.LG cs.PL
A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
我们描述了一种方法来验证实现的转换功能的程序，利用高阶表示的语法。在这种方法中，使用遗传Harrop公式的逻辑指定变换。一方面，这些规范直接作为实现，是Lambda Prolog语言中的程序。另一方面，它们可以用作Abella系统的输入，该系统允许我们证明关于它们的属性，从而证明关于实现的属性。我们认为，这种方法是特别有效的实现转换，分析绑定结构。我们通过在Lambda Prolog中描述对这种结构敏感的类型化闭包转换和代码提升等转换的简洁编码，并通过展示如何使用Abella证明其正确性来做到这一点。
2016-01-23 cs.LO cs.PL
A Categorical Framework for Program Semantics and Semantic Abstraction
本文提出一种用于抽象解释的函子方法，将解释表示为偏序集范畴中的oplax函子，并用lax自然变换表示抽象关系，从而将函子语义的优势引入语义抽象并讨论了其健全性。
2023-11-18 cs.PL math.CT
ShapeCoder: Discovering Abstractions for Visual Programs from Unstructured Primitives
Brown University（布朗大学）；Adobe Research（奥多比研究院）；University College London（伦敦大学学院）
ShapeCoder首次从非结构化图元中联合发现抽象函数和程序，通过识别网络与e-graph重写，在多个3D数据集上实现更优压缩与更少自由度。
2023-05-09 cs.AI cs.CV cs.GR
Representing Partial Programs with Blended Abstract Semantics
Massachusetts Institute of Technology（麻省理工学院）
从例子中合成程序需要在可能的程序的巨大的组合空间中搜索。在这个搜索过程中，一个关键的挑战是在程序可以执行之前表示部分编写的程序的行为，以判断它是否在正确的轨道上，并预测下一步在哪里搜索。我们介绍了一种通用的技术，用于表示部分编写的程序中的程序合成引擎。我们从抽象解释的技术，其中一个近似的执行模型是用来确定一个未完成的程序将最终满足一个目标规范的灵感。在这里，我们学习了一个近似的执行模型，它被实现为一个模块化的神经网络。通过构建组合程序表示，隐式编码的解释语义的底层程序设计语言，我们可以表示部分程序使用一个灵活的组合，具体的执行状态和学习的神经表示，使用学习的近似语义时，具体的语义是未知的（在未完成的部分程序）。我们表明，这些混合神经符号表示，使执行指导的合成器使用更强大的语言结构，如循环和高阶函数，并可以用来合成程序更准确地为一个给定的搜索预算比纯神经方法在几个领域。
2021-04-19 cs.AI cs.LG cs.PL
Abstracting Path Conditions
我们提出了一个基于符号执行的算法，对于一个给定的程序和一个给定的程序位置产生一个非平凡的必要条件输入值驱动程序执行到给定的位置。我们还提出了一个应用程序的必要条件，在当代的错误发现和测试生成工具。实验结果表明，该方法可以显著提高工具的性能.
2016-12-11 cs.LO cs.PL cs.SE
Symbolic Abstract Heaps for Polymorphic Information-flow Guard Inference (Extended Version)
在用于信息流控制的可靠的面向对象程序分析领域中，很少有方法采用堆的流敏感抽象来实现隐式流的精确建模。为了应对这一挑战，我们提出了一种新的符号抽象方法，用于在类Java程序中对堆进行建模。我们使用一个无存储的表示，参数化的家庭之间的关系的参考，提供不同程度的精度，根据用户的喜好。这使我们能够自动推断多态信息流警卫的方法，通过一个符号有限状态系统的可达性分析。我们用三个不同的关系族实例化堆抽象。我们证明了我们的方法的合理性，并通过使用IFSpec基准测试和现实生活中的应用程序与每个实例化堆域获得的精度和可扩展性进行比较。
2022-11-07 cs.CR cs.FL cs.PL
