Automated Transpilation of Imperative to Functional Code using Neural-Guided Program Synthesis (Extended Version)
虽然许多主流语言（如Java、Python和C#）越来越多地采用函数式API来简化编程并提高并行化/性能，但没有有效的技术可以用于使用这些API将现有的命令式代码自动转换为函数式变体。针对这一问题，本文提出了一种基于归纳程序合成的编译方法，以实现现有代码的现代化。我们的方法是基于这样的观察，即绝大多数的源/目标程序在此设置满足一个假设，我们称之为跟踪兼容性：不仅程序共享语法相同的低级别的表达式，但这些表达式也采取相同的值在相应的执行轨迹。我们的方法利用这一观察结果来设计一种新的神经指导合成算法，该算法（1）使用一种称为同源语法网络（CGN）的新型神经架构，（2）利用一种concolic执行形式来基于计算过程中出现的中间值修剪部分程序。我们已经在一个名为NGST 2的工具中实现了我们的方法，并使用它将命令式Java和Python代码转换为分别使用Stream和functools API的函数变体。我们的实验表明，NGST 2显着优于几个基线，我们提出的神经架构和修剪技术是实现良好的结果至关重要。
2022-03-18 cs.PL
Reactive Imperative Programming with Dataflow Constraints
数据流语言为动态应用程序中指定对象之间的约束提供了自然支持，其中程序需要有效地对环境的变化做出反应。研究人员长期以来一直在研究如何通过将它们嵌入到过程语言中来利用Challow-constraints。然而，以前的混合命令式/并行系统需要语法扩展或专门的数据类型库来将命令式程序绑定到并行求解器。在本文中，我们提出了一种新的方法，顺利地结合了这两种范式，而不会给程序员带来不必要的负担。在我们的框架中，程序员可以定义主机命令式语言的普通命令，这些命令强制执行存储在“反应式”内存位置中的对象之间的约束。反应对象可以是宿主语言中的任何合法类型，包括基本数据类型、指针、数组和结构。约束在每次输入内存位置改变时自动重新执行，让程序表现得像电子表格，其中某些变量的值取决于其他变量的值。通过改变宿主语言的基本操作的语义来读取和修改对象，从而透明地处理约束求解机制。我们提供了一个正式的语义和描述我们的技术到C/C++的一个具体实施例，展示了如何有效地实现它在传统的平台上使用现成的编译器。我们讨论了相关的应用反应的情况下，包括增量计算，观察者设计模式，和数据结构修复。我们的实现的性能相比，特设问题特定的变化传播算法和以语言为中心的方法，如自调整计算和主体/观察者通信机制，表明所提出的方法是有效的，在实践中。
2011-04-12 cs.PL
Leroy: Library Learning for Imperative Programming Languages
本研究提出Leroy系统，通过AST转换结合Stitch框架将库学习拓展至命令式语言，经Python子集验证可实现1.04倍代码压缩并能裁剪无效抽象，提升了代码可复用性与维护性。
2024-10-09 cs.PL
Terra: Imperative-Symbolic Co-Execution of Imperative Deep Learning Programs
Seoul National University（首尔大学）；FriendliAI；Samsung Research（三星研究院）；University of California, Berkeley（加州大学伯克利分校）
命令式编程允许用户轻松实现他们的深度神经网络（DNN），并已成为最近深度学习（DL）框架的重要组成部分。最近，已经提出了几个系统，结合命令式编程的可用性与符号图执行的优化性能。这样的系统将命令式Python DL程序转换为优化的符号图并执行它们。但是，它们不能完全支持命令式编程的可用性。例如，如果命令式DL程序包含没有相应符号表示的Python功能（例如，第三方库调用或不支持的动态控制流），它们无法执行程序。为了克服这一限制，我们提出了Terra，一个命令符号协同执行系统，可以处理任何命令DL程序，同时实现符号图执行的优化性能。为了实现这一点，Terra通过将DL操作与Python功能解耦来构建符号图。然后，Terra进行命令式执行以支持所有Python功能，同时将解耦操作委托给符号执行。我们评估了Terra的性能改进和覆盖率，其中包括针对几种DNN架构的十个强制性DL程序。结果表明，Terra可以加速所有十个命令式DL程序的执行，而最先进的系统之一AutoGraph无法执行其中的五个。
2022-01-23 cs.LG cs.PL
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
Kyoto University（京都大学）；The University of Tokyo（东京大学）
该研究提出ConSORT类型系统，结合精化类型与分数所有权类型，解决命令式程序中别名导致的强更新判定难题，实现自动推理工具，可验证含数据结构的非平凡程序。
2026-08-11 cs.PL
A Linear First-Order Functional Intermediate Language for Verified Compilers
我们提出了线性一阶中间语言IL验证编译器。IL是一种函数式语言，可以调用非确定性环境。我们给IL条款的第二个，命令式语义解释，并获得一个寄存器转移语言。对于命令式解释，我们建立了活变量的概念。基于活变量，我们制定了一个可判定的属性称为一致性，确保功能和命令的解释一个术语相吻合。我们制定了一个寄存器分配算法的IL，并证明其正确性。该算法将一个函数式IL程序转换为一个等价的命令式IL程序。正确性来自于这样一个事实，即算法在一致地重命名局部变量后达到了一个连贯的程序。我们证明了初始程序中的最大活变量数限制了最终相干程序中不同变量的数量。整个开发都在Coq中正式化。
2015-06-04 cs.PL
Building an IDE for the Calculational Derivation of Imperative Programs
在本文中，我们描述了一个IDE称为CAPS（计算助理编程规范）的交互式，计算推导的命令式程序。在构建CAPS的过程中，我们的目标是让非专家也能访问IDE，同时保留纸笔计算风格的整体风格。我们将讨论CAPS系统的整体架构、IDE的主要功能、GUI设计以及所涉及的权衡。
2015-08-17 cs.LO cs.PL
A Framework for Concurrent Imperative Programming
该框架提供了一个通用的并发命令式编程模型。程序被建模为形式语言，并发性被建模为交织（或混洗）运算符。这产生了一个简单而优雅的程序代数。该框架支持Dinsdale-Young等人的视图程序逻辑，它概括了各种类型系统和程序正确性的分离逻辑方法。它还验证了熟悉的操作演算在小步和大步的味道。程序逻辑相对于操作规则的一致性是直接建立的，并且不使用推导上的归纳。事实上，整个框架只使用简单的数学。参数化的状态，视图和基本命令，它可以实例化为各种具体的语言和设置。
2012-09-10 cs.LO cs.PL
Targeted Synthesis for Programming with Data Invariants
程序员经常维护隐式数据不变量，它们是程序中不同数据结构之间的关系。传统上，这种不变量是由程序员手动执行和检查的。这种特别的实践是困难的，因为程序员必须手动考虑破坏不变式的所有位置和配置。此外，隐式不变量在代码进化下是脆弱的：当不变量和数据结构发生变化时，程序员必须重复手动修复违反不变量的所有代码位置的过程。更好的方法是将数据不变量作为语言特性引入，并依赖语言支持来维护不变量。为了应对这一挑战，我们引入了目标合成，这是一种在编译时将数据不变量与不变量无关的命令式代码集成的技术。这种技术是不平凡的，由于两个不变的规范，以及一般的命令式代码的复杂结构。关键的见解是采取一种语言协同设计方法，涉及数据不变式语言和命令式语言。我们利用这一洞察力产生两个高层次的结果：第一，我们支持迭代器的语言，而不需要一般的量化推理，第二，我们推断复杂的不变保持补丁。我们评估这些索赔通过一种语言称为Spyder，一个核心演算的数据不变式的命令式迭代程序。我们评估的表现力和性能的Spyder的各种程序的灵感来自Web应用程序，我们发现，Spyder有效地编译和维护数据不变。
2019-10-25 cs.PL
Lambda the Ultimate SSA: Optimizing Functional Programs in SSA
静态单赋值（SSA）是命令式程序设计语言的现代优化编译器的主力。然而，函数式语言采用SSA的速度很慢，并且更喜欢使用基于最小lambda演算的中间表示，因为SSA无法表达高阶结构。我们利用一个新的SSA结构-区域-为了表达功能优化通过经典的SSA为基础的推理。区域优化目前依赖于ad-hoc分析和命令式程序的转换。这些特别的转换对于命令式语言来说已经足够了，因为区域的使用是有限的。相比之下，我们在函数IR中普遍使用区域来建模子表达式。这促使我们将区域优化系统化。我们将经典的SSA推理扩展到功能风格分析和转换的区域。我们实现了一个新的SSA+区域为基础的后端LEAN 4，定理证明，实现了一个纯粹的功能，依赖类型的程序设计语言。我们的后端是功能完整的，并在SSA框架内处理LEAN 4的函数中间表示λrc的所有构造。我们通过在MLIR中实现的基于SSA+区域的框架内优化λrc来评估我们提出的区域优化，并展示与当前LEAN 4后端的性能平价。我们相信我们的工作将为一个统一的优化框架铺平道路，该框架能够表示，分析和优化函数式和命令式语言。
2022-01-18 cs.PL
Proving Equivalence Between Imperative and MapReduce Implementations Using Program Transformations
分布式程序通常在MapReduce、Spark和Thrill等流行的功能框架中制定，但为此类框架编写高效的算法通常是一项不平凡的任务。由于大规模运行错误算法的成本可能很高，因此非常需要验证它们的正确性。我们建议采用现有的命令式参考实现作为MapReduce实现的规范。为此，我们提出了一种新的验证方法，其中一个命令和MapReduce实现之间的等价性建立了一系列的程序转换。在本文中，我们提出了如何等价框架可以用来证明之间的等价性的PageRank算法和MapReduce变种的强制性实现。八个单独的转换步骤分别介绍和解释。
2018-03-27 cs.LO cs.PL
Automating Proofs of Data-Structure Properties in Imperative Programs
我们考虑动态操作数据结构的自动推理问题。最先进的方法仅限于展开和匹配（U+M）范式，其中谓词在被视为未解释之前通过从其定义中导出的（解）折叠操作进行转换。然而，验证具有迭代循环和多个函数调用的程序的证明义务通常不会屈服于这种范式。我们的贡献是一个证明方法-超越U+M -执行自动公式重写处理以前遇到的义务，在每个证明路径作为可能的归纳假设。这使我们第一次能够系统地推理出实际方案核查所产生的各种义务。我们展示了我们的证明规则的力量，常用的引理，从而关闭现有的国家的最先进的系统中剩余的差距。另一个影响，可能更重要的是，我们的方法重新获得了组合推理的能力，并表明使用用户提供的引理不再需要现有的基准集。这不仅消除了提出适当引理的负担，而且还显著地提高了验证过程，因为引理应用与展开相结合，通常会导致非常大的搜索空间。
2014-07-23 cs.PL
Relational Cost Analysis for Functional-Imperative Programs
关系成本分析旨在正式建立两个项目评估成本差异的界限。作为一个特殊的情况下，也可以使用关系成本分析，以建立在两个不同的输入相同的程序的评估成本的差异的界限。执行关系成本分析的一种方法是使用关系类型和效果系统，该系统支持对两个程序的两次执行之间的关系进行推理。基于这一基本思想，我们提出了一个类型和效果的系统，称为ARel，推理数组操作，高阶函数命令式程序的相对成本。我们的方法的关键成分是一个新的轻量级类型细化规则，我们使用它来跟踪两个数组之间的关系（差异）。这种纪律结合霍尔风格的三元组内置的类型，使我们能够表达和建立精确的相对成本的几个有趣的程序，迫切需要更新他们的数据。
2019-09-24 cs.LO cs.PL
ImNet: An Imperative Network Programming Language
最新的网络架构之一是软件定义网络（SDN），其使用控制器设备来控制网络上的交换机集合。控制过程包括在交换机的流表上安装或卸载分组处理规则。本文提出了一种高级命令式网络程序设计语言，称为ImNet，以方便编写高效，但简单，由控制器执行的程序来管理交换机。ImNet结构简单，具有表达性，组合性和命令性。本文还介绍了一个操作语义的ImNet。文中还给出了在ImNet中构造的程序（及其操作语义）的详细实例。
2014-02-23 cs.NI cs.PL
Synthesizing Imperative Programs from Examples Guided by Static Analysis
Korea University（高丽大学）
我们提出了一种新的算法，综合了必要的程序介绍编程课程。给定一组输入输出示例和一个部分程序，我们的算法生成与每个示例一致的完整程序。我们的主要思想是结合枚举程序合成和静态分析，积极修剪出一个大的搜索空间，同时保证找到，如果有的话，一个正确的解决方案。我们已经实现了我们的算法在一个工具，称为SIMPL，并评估它的30个问题中使用的入门编程课程。结果表明，SIMPL能够在平均6.6秒内解决基准问题。
2017-06-13 cs.AI cs.PL
Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)
针对高阶命令式程序中现有两阶段规范机制精度不足的问题，本文提出支持多阶段的 Hoare 逻辑扩展，并开发了自动化高阶验证器 Heifer，以更精确地刻画未知函数参数和递归行为。
2024-07-02 cs.PL
Pleasant Imperative Program Proofs with GallinaC
提出GallinaC，将图灵完备命令式语言浅层嵌入Rocq证明助手的Gallina中，支持无界while循环，复用函数式证明策略，并通过链表反转证明验证可行性，正推进与Cminor的前向模拟。
2025-09-16 cs.LO cs.PL
A Type System Theory for Higher-Order Intensional Logic Support for Variable Bindings in Hybrid Intensional-Imperative Programs in GIPSY
我们描述了一个类型系统的平台称为一般内涵编程系统（GIPSY），旨在支持内涵程序设计语言的内涵逻辑和他们的强制性对应部分的内涵执行模型。在GIPSY中，类型系统在其编译器和运行时环境中粘合了内涵和命令式语言之间的静态和动态类型，以支持以内涵程序设计语言Lucid的各种方言编写的表达式的内涵求值。内涵使表达式明确考虑到多维的评估上下文，上下文是一个一流的值，服务于许多需要上下文概念来进行的应用程序。我们描述和讨论这样一个类型系统的属性和相关的类型论，以及GIPSY类型系统的语义，设计和实现的特殊性。
2009-06-22 cs.LO cs.PL
Verification of Imperative Programs by Constraint Logic Program Transformation
本文提出了一种基于约束逻辑程序变换（CLP）的方法来验证操作整数和数组的命令式程序的部分正确性。我们使用CLP作为一种元语言来表示命令式程序，它们的执行和它们的属性。首先，我们将命令式程序的正确性编码为CLP程序T定义的谓词“不正确”的否定。通过构造，“不正确”在T的最小模型中成立，当且仅当从初始配置执行prog最终在错误配置中停止。然后，我们对程序T应用一系列保持其最小模型语义的变换。这些转换是基于众所周知的转换规则，如展开和折叠，由适当的转换策略，如专业化和泛化。转换的目的是导出一个新的CLP程序TransfT，其中谓词“不正确”由以下定义：（i）事实“不正确”。'（在这种情况下prog是不正确的），或者由（ii）空子句集（在这种情况下prog是正确的）。在我们导出CLP程序使得（i）和（ii）都不成立的情况下，我们对变换进行了简化。由于问题是不可判定的，这个过程可能不会终止。我们通过例子表明，我们的方法可以应用在一个相当系统的方式，是适合自动化的程序验证领域的许多技术开发的程序转换。
2013-09-20 cs.LO cs.PL
JANUS: Fast and Flexible Deep Learning via Symbolic Graph Execution of Imperative Programs
Seoul National University（首尔国立大学）
深度神经网络的快速发展要求深度学习（DL）框架不仅要满足快速执行大型计算的要求，还要支持简单的编程模型，以快速实现和试验复杂的网络结构。然而，现有的框架无法同时在这两个部门中表现出色，导致优化性能和提高可用性的努力出现分歧。本文介绍了JANUS，一个系统，它结合了双方的优势，透明地转换成一个有效的可执行的符号化图的命令式DL程序编写的Python，事实上的脚本语言DL。JANUS可以将Python的各种动态特性，包括动态控制流、动态类型和不纯函数，转换为符号化的递归图的元素。实验表明，JANUS可以实现快速DL训练，利用基于符号图的DL框架所施加的技术，同时保持命令式DL框架的简单和灵活的可编程性在同一时间。
2019-03-11 cs.LG cs.PL
Rule-Based Graph Programs Matching the Time Complexity of Imperative Algorithms
University of Liverpool（利物浦大学）；University of York（约克大学）
通过增强GP 2编译器的图数据结构，实现了规则基图程序在连通性检测、无环性检测和单源最短路径问题上的时间复杂度与命令式实现相匹配。
2026-05-19 cs.PF cs.PL
Circular Programs and Self-Referential Structures
本文介绍利用循环程序和自引用结构在函数式语言中实现循环链表、双向链表、线索树和队列，并通过避免中间临时结构提升空间效率。
2024-03-04 cs.PL
Towards Hybrid Intensional Programming with JLucid, Objective Lucid, and General Imperative Compiler Framework in the GIPSY
纯Lucid程序是并发的，粒度非常细。顺序线程（ST）是为了扩大粒度而引入的函数;它们通过通用内涵编程系统（GIPSY）中的通信过程（CP）从服务器传递到工作器。JLucid程序将用于ST的Java代码与用于并行控制的Lucid代码相结合。因此，首先，在这篇论文中，我们描述了新的JLucid编译器生成ST和CP的方式。JLucid还引入了数组支持。进一步的探索经历了Lucid语言家族所经历的额外的转换，以支持在通用内涵程序设计语言（GIPL）和索引Lucid中使用Java对象及其成员：首先，以JLucid的形式允许使用伪对象，然后通过专门设计的Objective Lucid语言。通过讨论和实例，给出了ObjectiveLucid的语法和语义定义以及Java对象在内涵程序中的含义。最后，有许多有用的科学和实用程序是用Java以外的命令式程序设计语言编写的，例如C、C++、Fortran、Perl等。因此，提供一个框架来促进将这些语言包含到GIPSY中并由Lucid程序使用是明智的。为解决这一问题，提出了一个总的强制性框架及其具体实施。
2009-12-21 cs.PL cs.SE
On Decidable Growth-Rate Properties of Imperative Programs
2008年，本-阿姆拉姆、琼斯和克里斯蒂安森指出，对于一个简单的“核心”程序设计语言--一种有界循环的命令式语言，以及仅限于加法和乘法的算术--可以精确地决定一个程序是否具有某些增长率属性，即计算值或运行时间的多项式（或线性）界限。这项工作强调了核心语言在减轻程序属性臭名昭著的不可判定性方面的作用，以便处理可判定问题。一个自然而有趣的问题是，是否可以向核心语言添加更多的元素，提高其实用性，同时保持增长率属性的可判定性。特别是，所提出的方法无法处理将变量重置为零的命令。本文介绍了如何处理重置。分析是在一个逻辑风格（证明规则），其复杂性被证明是PSPACE-完全的（相比之下，没有重置，问题是PTIME）。分析算法以一种有趣的方式从以前的解决方案演变而来：焦点从证明一个界限转移到反驳它，算法自上而下而不是自下而上。
2010-05-04 cs.LO cs.PL
Tackling the Awkward Squad for Reactive Programming: The Actor-Reactor Model
针对响应式编程在真实应用中难以处理长时间计算、副作用及命令式与响应式代码协调的问题，提出 Actor-Reactor 模型，通过严格分离与数据流组合，在 Stella 语言中实现验证。
2023-06-21 cs.PL
Efficient compilation and execution of synchronous programs via type-state programming
针对同步程序编译中状态空间爆炸导致难生成高效可执行文件的问题，提出基于图重写规则的线性时间编译技术，结合C++模板元编程生成类型状态程序，实现了与现有水平相当的编译效率和二进制体积，执行速度提升31%-60%。
2025-08-02 cs.PL
Towards Safe Automated Refactoring of Imperative Deep Learning Programs to Graph Execution
本文提出一种基于张量分析的自动化重构方法，帮助开发者将命令式深度学习代码安全、高效地转换为图执行，以兼顾易用性与性能，并已在PyDev Eclipse IDE中实现。
2023-10-10 cs.PL cs.SE
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
Test Case Generation for Object-Oriented Imperative Languages in CLP
测试是软件开发过程的重要组成部分。测试用例生成（Test Case Generation，TCG）是自动生成应用于被测系统的测试用例集的过程。白盒TCG通常通过符号执行来执行，即，代替对正常值执行程序（例如，numbers），则程序在表示任意值的符号值上执行。在处理面向对象（OO）命令式语言时，符号执行变得具有挑战性，因为它必须能够回溯，复杂的堆分配数据结构应该在TCG过程中创建，并且必须考虑继承，虚拟调用和异常等特性。由于其固有的符号执行机制，我们追求在本文中，约束逻辑程序设计（CLP）有一个很好的未开发的应用领域在TCG。我们将支持我们的主张，开发一个完全基于CLP的框架，以TCG的面向对象的命令式语言，并通过评估它对一组具有挑战性的Java程序的相应实现。我们的方法的一个独特的特点是，它只使用CLP来处理所有的语言特征，而不需要开发特定的约束运算符（例如，对堆进行建模）。
2010-07-29 cs.PL cs.SE
A Semantics for Probabilistic Control-Flow Graphs
本文提出了一种新的操作语义的概率控制流图（pCFG）的概率命令式程序与随机分配和“观察”（或条件）语句。当控制从pCFG中的一个节点移动到另一个节点时，语义转换概率分布（在商店上）。我们将此语义的标准，预期转换，指称语义的结构化概率命令式程序，结构化程序翻译成（非结构化）pCFGs，并证明充分的翻译。这表明操作语义可以在不丢失信息的情况下使用，并且忠实于“预期”语义，因此可以用于推理，例如，转换的正确性（正如我们在配套文章中所做的那样）。
2017-11-07 cs.PL
Pifthon: A Compile-Time Information Flow Analyzer For An Imperative Language
实时信息流分析是保护私有数据机密性和完整性的一种很有前途的技术。在过去的几十年中，大量的信息流安全工具的运行时执行监视器或静态类型的系统的形式已经开发的程序设计语言来分析信息流的安全策略。然而，现有的流分析工具缺乏准确性和可用性，这是在实际应用开发中没有被广泛采用的主要原因。在本文中，我们提出了一个编译时的信息流分析的强制性程序的基础上的混合（可变+不可变）标签的方法，使用户能够检测到信息流的政策违反和修改程序，以克服违规行为。我们已经开发了一个信息流安全分析器的方言的Python语言，PyX，称为Pifthon使用上述方法。流分析器有助于识别与给定信息流策略（IFP）相对应的顺序PyX程序中可能的信息滥用。与文献中的其他方法相比，Pifthon具有明显的优势，例如减少了标签开销，改善了可用性，涵盖了广泛的PyX程序，包括终止和进展敏感通道。在经典无干扰条件下，证明了所提出的流动分析方法是合理的。最后，给出了使用Pifthon的案例和经验。
2021-03-10 cs.CR cs.PL
Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses
本文提出了一种基于规范自动转换的命令式程序正确性验证方法。给定一个程序prog，我们考虑形式为$\{φ\}$ prog $\{ψ\}$的部分正确性规范，其中断言$φ$和$ψ$是由可能递归的Horn子句的集合Spec定义的谓词，其前提中具有线性算术（LA）约束（也称为约束Horn子句）。验证方法包括在构造一组PC的约束Horn子句，其可满足性意味着$\{φ\}$ prog $\{ψ\}$是有效的。我们强调了一些限制的国家的最先进的约束霍恩子句求解方法，这里称为LA求解方法，证明可满足性的条款，通过寻找线性算术解释的谓词。特别是，我们证明了存在一些规格，不能证明有效的任何这些LA解决方法。这些规范要求证明一组包含非线性子句（即前提中有多个原子的子句）的受约束Horn子句的PC的可满足性。然后，我们提出了一个转换，称为线性化，PC转换成一组线性条款（即条款，在其前提中最多一个原子）。我们表明，几个规格，不能被证明是有效的LA解决方法，可以被证明是有效的线性化后。我们还提出了一种策略，用于执行线性化在一个自动的方式，我们报告的一些实验结果，通过使用我们的方法的初步实施。
2015-07-21 cs.LO cs.PL
WaveCert: Translation Validation for Asynchronous Dataflow Programs via Dynamic Fractional Permissions
针对数据流编译器转换异步程序易出错的问题，提出基于动态分数权限的翻译验证技术WaveCert，在RipTide CGRA架构的编译器中发现8个漏洞并验证了基准套件程序的编译正确性。
2024-04-12 cs.AR cs.PL
Challenges in Migrating Imperative Deep Learning Programs to Graph Execution: An Empirical Study
City University of New York (CUNY) Graduate Center（纽约城市大学研究生中心）；City University of New York (CUNY) Hunter College（纽约城市大学亨特学院）；Oakland University（奥克兰大学）
效率对于支持w.r.t.的响应至关重要。不断增长的数据集，特别是对于深度学习（DL）系统。深度学习框架传统上采用延迟执行风格的深度学习代码，支持符号化、基于图的深度神经网络（DNN）计算。虽然可扩展，但这样的开发往往会产生容易出错、不直观且难以调试的DL代码。因此，出现了更自然、更少出错的命令式DL框架，鼓励积极执行，但以牺牲运行时性能为代价。虽然混合方法的目标是“两全其美”，但在现实世界中应用它们的挑战在很大程度上是未知的。我们进行了一个数据驱动的分析的挑战-和由此产生的错误-参与编写可靠的，但性能的命令式DL代码通过研究250个开源项目，包括19.7 MPEG4，以及470和446手动检查的代码补丁和错误报告，分别。结果表明，混合：（i）易于API误用，（ii）可能导致性能下降-与其意图相反，（iii）由于执行模式不兼容，应用程序有限。我们提出了几个建议，最佳实践和反模式，以有效地混合命令式DL代码，可能有利于DL从业者，API设计师，工具开发人员和教育工作者。
2022-04-05 cs.LG cs.PL cs.SE
Speculative Automated Refactoring of Imperative Deep Learning Programs to Graph Execution
City University of New York (CUNY) Hunter College（纽约市立大学亨特学院）；CUNY Graduate Center（纽约市立大学研究生中心）；Oakland University（奥克兰大学）
针对命令式深度学习程序，提出基于静态分析和推测性关键词分析的自动化重构方法，将其转为图执行以提升性能，在19个项目中平均加速2.16倍。
2025-10-06 cs.AI cs.PL cs.SE
AsyncTaichi: On-the-fly Inter-kernel Optimizations for Imperative and Spatially Sparse Programming
Taichi Graphics（太极图形）；MIT CSAIL（麻省理工学院计算机科学与人工智能实验室）；Tsinghua University（清华大学）
利用空间稀疏性已经成为加速3D计算机图形应用的流行方法。空间稀疏的数据结构和高效的稀疏内核（如对活动体素的并行模板操作）是实现高性能的关键。现有的工作集中在提高性能在一个单一的稀疏计算内核。我们表明，一个系统，超越了一个单一的内核，加上额外的特定领域的稀疏数据结构分析，开辟了令人兴奋的新空间，优化稀疏计算。具体来说，我们提出了一个特定于域的数据流图模型的命令式和稀疏计算程序，它描述了内核的关系，并使易于分析和优化。与暴露宽内核窗口的异步执行引擎相结合，内核间优化器可以执行有效的稀疏计算优化，例如消除不必要的体素列表生成和删除体素激活检查。这些特定于域的优化进一步为经典的通用优化让路，这些优化最初难以直接应用于具有稀疏数据结构的计算。在没有任何计算代码修改的情况下，我们的新系统导致$4.02\times$更少的内核启动和$1.87\times$加速我们的GPU基准测试，包括欧拉网格，拉格朗日粒子，网格和自动微分的计算。
2021-06-22 cs.AI cs.GR cs.PL
Algorithmic Verification of Single-Pass List Processing Programs
我们引入了流数据串转换器，其在线性时间中以单次从左到右通过将输入数据串映射到输出数据串。数据字符串是数据值的（无界）序列，标记有有限集合中的符号，在一个潜在的无限数据域上，只支持相等和排序的操作。传感器使用有限的状态集、在数据域上的有限的变量集和在数据串上的有限的变量集。在每一步，它可以根据下一个输入符号做出决定，更新其状态，记住其数据变量中的输入数据值，并通过连接数据串变量和由数据变量形成的新符号来更新数据串变量，同时避免重复。我们建立的问题，检查两个流式传感器的功能等效性，并检查是否流传感器满足前/后验证条件流接收器指定的输入/输出数据串，在PSPACE。我们确定了一类命令和一类函数程序，操纵列表的数据项，可以有效地转换为流数据串换能器。命令式程序通过改变堆节点的下一个指针和添加新节点来动态修改单链堆。主要限制指定了下一个指针如何用于遍历。我们还确定了一个表达等效的函数程序片段，遍历一个列表使用语法限制递归调用。我们的研究结果导致算法的断言检查和检查功能等价的两个程序，写在不同的编程风格，常用的例程，如插入，删除，和反向。
2011-02-14 cs.PL
An Executable Specification of Oncology Dose-Escalation Protocols with Prolog
本文提出了首个以纯Prolog程序实现的3+3肿瘤剂量递增方案可执行规范，通过CLP(Z)约束的预期后悔场景推导操作，为试验前验证和在线决策提供稳健支持。
2024-02-13 cs.PL
Gobra: Modular Specification and Verification of Go Programs (extended version)
Go是一种越来越流行的系统程序设计语言，特别是针对并发和分布式系统。Go语言与其他命令式语言的不同之处在于，它通过goroutine提供了结构化的子类型和轻量级的并发性以及消息传递通信。这些特性的组合为静态验证提出了有趣的挑战，最突出的是可变堆和高级并发原语的组合。我们提出Gobra，一个模块化的，演绎的程序验证器，证明内存安全，崩溃安全，数据竞争自由，和用户提供的规范。Gobra基于分离逻辑，支持Go语言的一个大子集。它的实现将带注释的Go程序转换为Viper中间验证语言，并使用现有的基于SMT的验证后端来计算和履行证明义务。
2021-05-28 cs.PL
A Preliminary Data-driven Analysis of Common Errors Encountered by Novice SPARC Programmers
答案集编程（ASP），逻辑编程的现代发展，使计算与STEM学科的自然整合。这种整合解决了K-12教育中广泛承认的挑战，基于ASP的整合的早期经验结果是有希望的。虽然与命令式程序设计语言相比，ASP被认为是一种简单的语言，但编程错误仍然是学生的一个重大障碍。这对于K-12学生来说尤其如此，他们是ASP的新手用户。对错误进行分类并测量其难度已经使人们对Java等命令式语言有了深入的了解。然而，很少有人知道的类型和困难的K-12学生使用ASP遇到的错误。为了解决这个问题，我们收集了高中学生在一个4节课的ASP语言教学研讨会上提交的程序。从这个数据集中的错误消息中，我们确定了一个错误类的集合，并测量每个类出现的频率以及解决的难度。
2022-08-05 cs.CY cs.PL
Extending Isabelle/HOL's Code Generator with support for the Go programming language
本工作为Isabelle/HOL的代码生成器新增Go语言作为第五种目标语言，通过命令式构造模拟函数式特性，并以附加库形式提供支持。
2024-09-19 cs.LO cs.PL
Interacting via the Heap in the Presence of Recursion
几乎所有现代命令式程序设计语言都包含动态操作堆的操作，例如通过分配和释放对象，以及通过更新引用字段。在递归过程和局部变量的存在下，程序与堆的交互可能变得相当复杂，因为可以使用局部变量在调用堆栈上分配无限数量的对象，或者匿名地使用引用字段在堆上分配对象。因此，一般来说，静态分析是不可判定的。在本文中，我们研究了验证的递归程序与无界分配的对象，在一个简单的命令式语言堆操作。我们提出了一种改进的语义，这种语言，使用的抽象是精确的。对于任何具有有界可见堆的程序，这意味着在任何执行点从变量可到达的对象数量是有界的，这种抽象是其行为的有限表示，即使在状态中可能出现无限数量的对象。因此，对于这样的程序，模型检验是可判定的。最后，我们介绍了一个规约语言的时间属性的堆，并讨论了模型检验这些属性对堆操作程序。
2012-12-17 cs.LO cs.PL
Inferring Types for Parallel Programs
消息传递接口（MPI）框架广泛用于实现具有高度并行性的命令式程序。PARTYPES方法为类MPI程序提出了一种行为类型规则，其中一种类型描述了整个程序所遵循的通信协议。良好类型的程序保证不会出现死锁。在本文中，我们描述了一个类型推断算法的原始系统的一个子集，该算法允许静态提取一个MPI程序从其源代码的类型。
2017-04-11 cs.LO cs.PL
On completeness of logic programs
程序正确性（在命令式和函数式编程中）在逻辑编程中分为正确性和完整性。完整性意味着一个程序产生了它的规范所要求的所有答案。很少有人致力于对完备性的推理。本文给出了定规划完备性的几个充分条件。我们还研究了在SLD树的某些修剪情况下（例如，由于使用切割）保持完整性。我们将逻辑编程视为一种声明性的范例，尽可能地从任何操作语义中抽象出来。我们认为，所提出的方法是足够简单的应用，可能在一个非正式的水平，在实际的Prolog编程。我们指出近似规格的重要性。
2014-11-11 cs.LO cs.PL
NetRep: Automatic Repair for Network Programs
由于理解各种网络模块和复杂的数据结构通常是耗时的，因此对于开发人员来说，开发命令式网络程序是一项具有挑战性的任务。为了解决这一问题，本文提出了一种从单元测试中自动修复网络程序的技术。具体地说，给定一个有故障的网络程序和一组单元测试作为输入，我们的方法通过符号推理定位故障，并合成一个补丁，使修复后的程序可以通过所有的单元测试。它应用特定于领域的抽象来简化网络数据结构，并利用模块化分析来促进功能摘要的符号分析重用。我们在一个名为NetRep的工具中实现了所提出的技术，并在根据现实世界的软件定义网络控制器改编的10个基准测试上对其进行了评估。评估结果表明NetRep修复网络程序的有效性和效率。
2021-10-20 cs.PL cs.SE
Enabling Operator Reordering in Data Flow Programs Through Static Code Analysis
在许多大规模并行数据管理平台中，程序被表示为连接在数据流中的小的命令式代码段。这种流行的抽象使得很难应用关系DBMS和其他使用代数编程抽象的系统所采用的代数重新排序技术。我们提出了一种基于反向数据和控制流分析的代码分析技术，该技术从用户代码中发现一组属性，这些属性可用于在此设置中模拟代数优化。
2013-01-17 cs.DB cs.DC cs.PL
