Verified Self-Explaining Computation
常见的编程工具，如编译器，调试器和IDE，主要依赖于分析程序代码的能力，以推断其行为和属性。在验证编译器和静态分析方面已经做了大量的工作，但是在验证诸如程序切片之类的动态分析方面的工作却少得多。最近，一个新的数学框架切片介绍，其中向前和向后切片是双重的意义上说，他们构成了伽罗瓦连接。本文形式化了一种简单命令式程序设计语言的前向和后向动态切片算法，并使用Coq证明助手形式化地验证了它们的对偶性。
2019-07-12 cs.PL
Slicing of Probabilistic Programs based on Specifications
本文提出了第一个基于规格说明的概率程序切片方法。我们表明，当概率程序伴随着他们的规格的形式的前和后条件，我们可以利用这种语义信息，以产生规范保护片严格更精确的比传统技术的基础上产生的切片数据/控制依赖。为了实现这一目标，我们的技术是基于后向传播的条件通过最大的预期望Transformer-Dijkstra最弱的前提条件Transformer的概率对应。该技术是终止敏感的，允许保留的部分以及总的正确性的概率程序w.r.t.他们的规格。它是模块化的，具有局部推理原则，并被正式证明是正确的。作为我们的技术的基本技术成分，我们设计并证明了健全的验证条件生成器，用于建立概率程序的部分和全部正确性，这些程序本身就很有趣，可以在其他地方用于其他目的。在实践方面，我们证明了我们的方法的适用性，通过一些说明性的例子和案例研究，从概率建模领域。我们还描述了一个算法，用于计算最少的切片之间的空间，我们的技术。
2022-05-07 cs.PL
Enhancing the performance of Decoupled Software Pipeline through Backward Slicing
多核处理器中可用内核数量的快速增加并不一定直接导致性能的相应提高：用传统语言（如C）编写的程序需要仔细重构，最好是自动重构，然后才能在改进的运行时间中观察到好处。即使这样，也很大程度上取决于原始程序的并发执行的内在能力。本文的主题是去耦软件管道（DSWP）和（向后）切片的互补技术的综合效果带来的性能提升。DSWP从循环体中提取线程级并行性，方法是将循环体分解为多个阶段，然后以流水线方式执行：实际上是跨越控制链。另一方面，切片沿着控制链切割程序，梳理出依赖于不同变量（或位置）的更精细的线程。取决于不同变量的部分。本文的主要贡献是证明DSWP的应用，其次是切片提供了显着的改进DSWP单独，特别是当有一个循环进行的依赖，防止应用程序的简单DOALL优化。实验结果表明，一个因素的改善？1.6对于DSWP +切片超过DSWP单独和一个因素？2.4对于原始顺序代码的DSWP +切片。
2015-01-27 cs.PL
Distributed Data and Programs Slicing
本文提出了一种新的技术，数据切片的分布式程序上运行的层次结构的机器。数据切片可以实现为一种程序转换，将层次结构中的机器堆划分为独立的区域。在每台机器的每个区域内，指针保留原始堆层次结构中的原始指针结构。基本类型的每个堆组件（例如，整型）仅进入堆之一的区域。所提出的技术具有推理规则系统的形状。此外，本文还提出了一种结构简单的类型系统来判定分布式程序的类型可靠性。使用这种类型系统，数学证明，建议的切片技术保持类型属性概述了本文。
2014-02-24 cs.PL cs.SE
Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)
RWTH Aachen University（亚琛工业大学）
本文提出通过切片技术提升概率程序验证的诊断能力，通过Brutus实现高效错误定位与验证提示。
2025-12-24 cs.PL
SymPas: Symbolic Program Slicing
程序切片是一种通过关注程序行为的选定方面来简化程序的技术。当前主流的静态切片方法在PDG（程序依赖图）或SDG（系统依赖图）上操作，但是这些友好的图表示对于一些用户来说可能是昂贵的并且容易出错。在本文中，我们试图研究一个轻量级的静态程序切片的方法，称为符号程序切片（Symbolic Program Slicing，SymbolPas），它的工作原理是对LLVM（低级虚拟机）的一个简单的分析。在我们的SymPas方法中，切片是符号化存储的，而不是重新分析的过程（参见。程序摘要）。SymPas不是多次重新分析过程以找到每个调用上下文的切片，而是计算单个符号（或参数化）切片，该切片可以在调用站点实例化，避免重新分析;它在LLVM中实现以对其中间表示（IR）执行切片。为了比较，我们系统地适应IFDS（过程间有限分布子集）分析和基于SDG的切片方法（SDG-IFDS）静态IR切片程序。在开源和基准程序上进行评估，与后向SDG-IFDS相比，我们的后向SymPas显示出时间成本降低了6倍，空间成本降低了4倍，因此更高效。此外，结果表明，在研究了66个程序的切片后，大小范围高达336，800条IR指令，SymPas具有高度的大小可伸缩性。
2019-03-13 cs.LO cs.PL cs.SE
Imperative Functional Programs that Explain their Work
程序切片提供了说明如何从输入生成程序输出的解释。我们建立在Perera等人在先前工作中引入的方法上，其中动态切片被定义为纯高阶函数程序作为部分输入和部分输出的格之间的伽罗瓦连接。我们将这种方法扩展到结合高阶编程与引用和异常的命令式函数程序。我们提出了我们的方法的正确性和最优性的证明和概念验证的实施和实验评估。
2017-05-22 cs.PL
An approach to find dynamic slice for C++ Program
面向对象程序设计被认为是程序开发和维护中最有前途的方法。面向对象程序的一个重要特征是其可重用性，可重用性可以通过类或可重用组件的继承来实现，动态程序切片是一种在调试时将错误缩小到程序相关部分的有效技术。给定一个切片标准，动态切片只包含那些真正影响切片标准中变量的语句。提出了一种基于依赖分析的面向对象程序动态切片方法。它利用目标程序的控制依赖图和其它静态信息来减少程序执行过程中需要跟踪的信息。在本文中，我们提出了一种方法来找到面向对象程序的动态切片，我们正在寻找对象的切片和函数重载的情况下。
2010-06-14 cs.PL
A Theory of Slicing for Probabilistic Control-Flow Graphs
我们提出了一个理论切片概率命令式程序-包含随机分配，和“的”语句（条件）-表示为概率控制流图（pCFGs），其节点修改概率分布。我们表明，这样的表示允许直接适应的标准机械，如数据和控制依赖，postdominators，相关变量等的概率设置。我们分离的规范切片从其实现：首先，我们开发的句法条件，切片必须满足;其次，我们证明，任何这样的切片是语义正确的;最后，我们给出了一个算法来计算最少的切片。为了生成更小的切片，我们还可以利用某些循环将（几乎）总是终止的知识。我们的句法条件的一个关键特征是，它们涉及两个不相交的切片，使得一个切片的变量在概率上独立于另一个切片的变量。这直接导致了概率切片的正确性证明。在同伴的文章中，我们充分的pCFGs的语义相对于标准的结构化概率程序的语义。
2017-11-07 cs.PL
A Theory of Changes for Higher-Order Languages - Incrementalizing λ-Calculi by Static Differentiation
如果一个昂贵的计算的结果被输入的一个小变化所无效，旧的结果应该被增量地更新，而不是重新执行整个计算。我们通过它们的衍生物来增加程序。派生程序将程序输入的变化直接映射到程序输出的变化，而不需要重新执行原始程序。我们提出了一个程序转换程序的衍生物，这是完全静态和自动的，支持一流的功能，并产生衍生物服从标准优化。我们证明了在Agda中对于一族简单类型的λ演算的程序转换是正确的，这些演算由基类型和原语参数化。一个精确的接口指定了增量化所选原语所需的内容。我们调查性能的案例研究：我们在Scala实现的程序转换，一个插件，并提高性能的一个重要的程序的数量级。
2013-12-02 cs.PL
Static Program Slicing Using Language Models With Dataflow-Aware Pretraining and Constrained Decoding
Department of Computer Science, University of Manitoba（曼尼托巴大学计算机科学系）；School of Engineering and Computer Science, Concordia University（Concordia大学工程与计算机科学学院）；School of Computer Science, University of Windsor（温莎大学计算机科学学院）
本文提出Sliceformer，通过数据流感知预训练和约束解码改进静态程序切片，提升依赖建模精度和减少生成幻觉，实验显示在Java和Python基准上精确匹配提升22%。
2026-05-10 cs.AI cs.PL cs.SE
Some Issues on Incremental Abstraction-Carrying Code
抽象承载代码（ACC）最近被提出作为用于证明承载代码（PCC）的框架，其中代码供应商提供程序连同抽象（或程序的抽象模型），其有效性需要遵守预定义的安全策略。因此，抽象起到了安全证书的作用，其生成（和验证）由定点分析器自动执行。PCC的现有方法是在消费者读取并验证整个程序w.r.t.以非增量的方式一次获得完整的证书。在这篇摘要中，我们概述了增量ACC的主要问题。特别是，在逻辑编程的背景下，我们讨论了增量证书的生成和（可信）程序的不可信更新的增量检查算法的设计，即，当生产者提供先前验证的程序的修改版本时。通过更新，我们指的是对程序的任何任意更改，即，用新谓词扩展程序，删除现有谓词，并用新版本替换现有谓词。我们还讨论了每种更新如何影响增量扩展的准确性和正确性。
2007-01-17 cs.PL
Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)
RWTH Aachen University（亚琛工业大学）
本文提出一种简单程序化方法，通过增量差异分析概率程序的多种目标，如高矩、阈值概率等，利用现有推理方法实现统一分析。
2026-03-02 cs.PL
Slicing Concurrent Constraint Programs
并发约束编程（CCP）是一个声明式的并发模型，其中代理通过告诉和询问共享存储中的约束（信息片段）进行交互。以前的一些作品已经开发了（近似）CCP语言的声明式调试器。然而，调试并发程序的任务仍然很困难。在本文中，我们定义了一个动态切片CCP，我们表明它是一个有用的伴侣工具，现有的调试技术。我们的技术首先考虑一个部分计算（跟踪），显示存在的错误。通常，这种跟踪中的信息量是压倒性的，用户很容易迷失方向，因为她不能专注于bug的来源。我们的切片器允许标记计算状态的一部分，并帮助用户消除大部分冗余信息，以突出错误。我们表明，这种技术可以定制CCP的定时变量。我们还开发了一个原型实现免费提供实验。
2017-02-10 cs.LO cs.PL
DeCo: A Core Calculus for Incremental Functional Programming with Generic Data Types
TU Darmstadt（达姆施塔特工业大学）；National Research Center for Applied Cybersecurity ATHENE（国家应用网络安全研究中心 ATHENE）
本文提出DeCo核心演算，通过静态增量泛化用户自定义数据类型上的领域特定操作，实现更细粒度的增量计算，并证明其正确性。
2026-02-24 cs.PL
Incremental Live Programming via Shortcut Memoization
本文提出Chordata，一种基于快捷记忆化的增量式程序解释器，通过学习重复计算模式提升实时编程效率，实验证明其在处理复杂程序时具有显著加速效果。
2026-03-20 cs.PL
Using Standard Typing Algorithms Incrementally
现代语言配备了静态类型检查/推理，帮助程序员保持干净的编程风格并减少错误。然而，不断增长的程序规模及其持续发展需要构建快速高效的分析器。一个很有前途的解决方案是增量式，这样只需要重新输入程序中新的部分，而不是整个代码库。我们提出了一个算法模式驱动的增量类型化算法，利用现有的，标准的没有变化的定义。我们的方法是一种灰盒方法，这意味着只需要输入的形状、结果的形状和一些特定于领域的知识来实例化我们的模式。在这里，我们提出了我们的方法的基础，我们在工作中得到三个不同的增量类型化算法。前两个实现了函数语言的类型检查和推理。最后一个是对命令式语言进行类型检查，以检测信息流和非干扰。我们评估了我们的建议，一个增量类型检查器的原型实现。我们的实验表明，增量地使用类型检查器（几乎）总是有益的。
2018-11-27 cs.PL
Incremental Computation with Names
在过去的三十年中，在开发通用的、基于语言的增量计算方法方面取得了重大进展，其目的是在输入改变时有效地更新计算结果。这种方法的一个关键设计挑战是如何为广泛的程序提供有效的增量支持。在本文中，我们认为，一流的名字是一个关键的语言特征，有效的增量计算。名称标识了要在程序的不同运行中重用的计算，使它们成为第一类给了程序员对重用的高度控制。我们展示了名称的好处，提出NOMINAL ADAPTON，ML类语言的增量计算的名称。我们描述了如何使用NOMINAL ADAPTON来有效地递增几个标准编程模式-包括映射，折叠和展开-并展示了如何构建高效的，递增的概率树和尝试。由于NOMINAL ADAPTON的实现是微妙的，我们将其形式化为核心演算，并证明它是从头开始一致的，这意味着它总是产生与简单地重新运行计算相同的答案。最后，我们证明了NOMINAL ADAPTON可以提供大的加速比从头开始计算和ADAPTON，以前的国家的最先进的增量计算系统。
2021-03-23 cs.PL
Refinement types for precisely named cache locations
许多用于增量计算的程序设计语言技术为高速缓存的信息使用程序员指定的名称。在运行时，每个名称标识动态数据值或子计算的“缓存位置”;总之，这些缓存位置选择指导更改传播和增量（重新）执行。当一个缓存位置最多标识一个值或子计算时，我们称它为精确的;我们称所有其他名称为不精确的或模糊的。至少，缓存位置名称必须精确，以确保更改传播正确工作;然而，在增量程序中静态推理名称仍然是一个悬而未决的问题。作为第一步，本文定义并解决了精确的名称问题，在这里我们验证了增量程序与显式名称使用它们精确。为了做到这一点，我们给出了一个细化类型和效果系统，并证明它是合理的（每个类型良好的程序都精确地使用名称）。我们还通过验证计算增量序列和集合的高效表示的示例程序来证明这种类型系统的表达能力。除了验证这些程序，我们的类型系统还描述了它们的动态命名策略，例如，用于图书馆文档。
2017-10-21 cs.PL
Fixing Incremental Computation: Derivatives of Fixpoints, and the Recursive Semantics of Datalog
最近已经使用程序的变化结构和导数的概念来研究增量计算，其中函数的导数允许基于对其输入的改变来更新函数的输出。我们概括改变结构改变行动，并研究其代数性质。我们开发了计算机科学中常见结构的变化动作，包括有向完全偏序和布尔代数。然后，我们将展示如何计算不动点的导数。这使我们能够执行增量评估和维护递归定义的功能与特定的应用程序，以广义的Datasheet程序。此外，与以前的结果不同，我们的技术是模块化的，因为它们很容易应用到Datasheet的变体和其他程序设计语言。
2018-11-23 cs.PL
Sliced Slices: Separating Data and Control Influences
后向切片在程序理解、调试和程序分析的扩展中得到了广泛的应用。对于大型程序，常规向后切片的大小约为程序大小的25%。这可能太大而没有用处。我们的调查表明，在一般情况下，切片的大小的影响更多的控制流达到切片标准的计算，而不是由管理的值相关的切片标准的计算。我们通过定义数据切片和控制切片来区分两者，这两者都小于通过组合两者可以获得的常规切片。这很有用，因为对于许多应用程序来说，单独的数据或控制片就足够了。我们的实验表明，超过50%的情况下，数据切片小于10%的程序大小。此外，计算数据或控制切片的时间与计算传统切片的时间相当。
2014-07-18 cs.PL cs.SE
One Tool, Many Languages: Language-Parametric Transformation with Incremental Parametric Syntax
我们提出了一种新的方法来构建源到源的转换，可以运行在多种程序设计语言，基于一种新的方式表示程序称为增量参数语法。我们在Cubix系统中的Haskell中实现了这种方法，并为C，Java，JavaScript，Lua和Python构建了增量参数语法。我们展示了一个运行在所有这些转换上的全程序重构工具，以及三个较小的转换，每个转换运行在几个转换上。我们的评估表明，（1）一旦编写了转换，几乎不需要为新语言配置它;（2）根据我们人类研究的参与者，以这种方式构建的转换输出可读代码，保留原始结构;（3）我们的转换仍然可以处理语言的角落情况，如编译器测试套件所验证的。
2018-10-01 cs.PL
Incremental units-of-measure verification
提出一种支持增量标注的轻量级静态验证系统，通过生成全局约束系统为 Fortran 程序推断和检查多态 units-of-measure 规范，实现模块独立求解以扩展至大型项目。
2024-06-04 cs.PL
Proving Almost-Sure Termination of Probabilistic Programs via Incremental Pruning
经典的命令式程序的实值随机变量和随机分支的扩展产生了概率程序。终止问题是此类程序最基本的活性性质之一。定性（也称为几乎肯定）终止问题询问给定程序是否以概率1终止。排序函数为非概率规划的终止提供了一种完善的方法，而将其推广到概率规划则是通过排序上鞅（Ranking Supermartingales，RSM）实现的。RSM已经扩展到字典式RSM，以处理涉及控制流结构的程序，以及组合方法。现有的基于RSM的方法有两个主要的局限性：首先，字典式的基于RSM的方法需要一个强的非负性假设，这并不总是需要满足。现有的基于RSM的算法方法的第二个关键限制是它们依赖于预先计算的不变量。依赖于预先计算的不变量的主要缺点是不一致性和低效率的权衡：弱不变量可能不足以让RSM证明终止，而使用强不变量会导致计算效率低下。我们的贡献是双重的：首先，我们展示了如何放松强非负性条件，并仍然提供可靠性保证几乎肯定终止。其次，我们提出了一个增量的方法，计算字典的RSM的过程中进行迭代修剪的程序，已经被证明是终止的部分，与安全证明。特别是，我们的技术不依赖于强大的预先计算的不变量。我们目前的实验结果表明，我们的方法的适用性，从文献中的概率程序的例子。
2021-08-06 cs.PL
An Incremental Algorithm for Algebraic Program Analysis
本文提出一种增量代数程序分析方法，通过树结构表示路径表达式并高效更新程序属性，在DaCapo基准的13个Java应用上实现160X至4761X的加速。
2024-12-14 cs.PL cs.SE
Incremental Computation: What Is the Essence?
本文概述了增量计算的本质——增量化，即微积分求导的离散对应物，并提出了以增量化为核心的 Iterate-Incrementalize-Implement 系统化方法，用于程序与算法的设计与优化。
2025-10-13 cs.PL
Incremental and Modular Context-sensitive Analysis
大型代码库的上下文敏感全局分析可能是昂贵的，这可能使其在软件开发期间的使用不切实际。然而，在许多情况下，修改很小并且孤立于几个组件中，并且希望尽可能多地重用先前的分析结果。迄今为止，这已经通过增量全局分析定点算法实现，这些算法在精细的粒度级别上实现成本降低，例如程序行的更改。然而，这些细粒度技术并不直接适用于模块化程序，也不是为了利用模块化结构而设计的。本文描述，实现，并评估一个算法，执行有效的上下文敏感的分析增量模块化分区的程序。实验结果表明，所提出的模块化算法表现出显着的改善，在时间和内存消耗，相比现有的非模块化，细粒度增量分析技术。此外，由于所提出的分析信息的模块间传播，我们的算法也优于传统的模块化分析，即使从头开始分析。
2020-12-18 cs.PL
Incremental Computation for Efficient Programmable Inference in Probabilistic Programs
Massachusetts Institute of Technology（麻省理工学院）；Yale University（耶鲁大学）
提出基于增量计算的方法，将概率程序编译为确定性密度函数，并通过增量λ演算实现函数式程序的增量计算，以加速蒙特卡洛推理，支持非参数模型，并保证正确性。
2026-06-03 cs.LO cs.PL stat.CO
Incremental Bidirectional Typing via Order Maintenance
本文提出一种基于顺序维护数据结构的增量双向类型推导系统，通过指针连接绑定变量与绑定位置并优先化更新传播，在 Agda 中证明其等价于朴素重分析，并在 OCaml 实现中取得 275.96 倍加速。
2025-04-11 cs.PL
Fungi: Typed incremental computation with names
增量计算试图利用输入随时间的相似性，重用不受输入变化影响的工作。为了在通用编程设置中最大化这种重用，程序员需要一种机制来识别随时间对应的（数据和子计算的）动态分配。我们提出真菌，一个类型化的函数式语言的增量计算的名称。与以前的增量计算通用语言不同，Fungi的名称概念是正式的、通用的和静态可验证的。真菌的类型和效果系统允许程序员编码（程序特定的）关于名称的局部不变量，并使用这些不变量为他们的组合程序建立全局唯一性，正确使用名称的属性。我们证明了良好类型的真菌程序尊重全球唯一性。我们派生了类型和效果系统的双向版本，并在Rust中实现了Fungi的原型。我们将真菌应用到一个增量集合库中，表明它在实践中具有表达能力。
2018-08-20 cs.FL cs.LO cs.PL
miniAdapton: A Minimal Implementation of Incremental Computation in Scheme
我们描述了miniAdapton的完整Scheme实现，它实现了Adapton系统的核心功能，用于增量计算（也称为自调整计算）。像Adapton一样，miniAdapton允许程序员安全地组合突变和记忆。miniAdapton建立在一个更简单的系统microAdapton之上。miniAdapton和microAdapton都设计成易于理解、扩展和移植到Scheme以外的主机语言。我们还介绍了adapton变量，这是Adapton中用于表示表达式的变量的新接口。
2016-09-17 cs.PL
CheckedCBox: Type Directed Program Partitioning with Checked C for Incremental Spatial Memory Safety
空间内存安全违规仍然是C程序的一个主要问题。Anchoked-C是一种安全的C语言方言，并扩展了它的指针类型和注释，以向后兼容的方式保证空间内存安全，允许检查指针和常规（未检查）指针类型的混合。然而，未经检查的代码漏洞可能会违反经检查的代码的空间安全保证。我们提出了一个灵活的，类型导向的程序分区机制，以masked-C，通过增强masked-C类型系统与污染的类型，使灵活的分区的程序到检查和未检查的区域，在这样的方式，未检查的区域代码不会影响空间安全检查区域。我们形式化我们的类型系统，并证明了非崩溃和非暴露性质的一个良好的类型化的PockedCBox程序。我们以一种可配置的方式实现了WebkedCBox，这使我们能够使用现有的沙箱机制（例如WebAssembly）来执行程序。因此，在这样做的过程中，通过有效地分区程序，AnchikedCBox已经防止了四个已知的漏洞。
2023-02-03 cs.CR cs.PL
Unbounded Software Model Checking with Incremental SAT-Solving
提出了一种基于增量SAT求解的无界软件模型检验方法，用于发现C语言程序中的错误。而不是使用传统的假设为基础的API增量SAT求解器，我们使用的DimSpec格式，用于SAT的自动规划。DimSpec公式由四个CNF公式组成，分别表示过渡系统的初始状态、目标状态和中间状态以及每对相邻状态之间的关系。我们提出了一种新的工具，称为LLUMC编码的存在下，在C程序中的某些错误到一个DimSpec公式，它可以解决增量SAT为基础的DimSpec求解器或IC3算法不变检查。我们评估的情况下，基于SAT的模型检验的增量SAT求解和IC3算法的方法。我们表明，我们的编码还覆盖了大型和无限循环，同时仍然保持了可行的时间性能，从而扩展了有界模型检查器的功能。此外，我们证明了我们的方法提供了机会，通过利用并行SAT求解生成运行时优化。
2018-02-12 cs.PL cs.SC
