A Term-Rewriting Semantics for Imperative Style Programming
术语重写系统具有简单的语法和语义，并且便于正确性证明。然而，它们在工业界或学术界并不像命令式语言那样受欢迎。我们定义了一个术语重写为基础的抽象程序设计语言与一个命令式的风格和精确的语义，允许程序翻译成高效的命令式语言，以获得证明的正确性与高效的执行。这种语言的目的是促进翻译成正确的程序在命令式语言的赋值语句，迭代，递归，数组，指针和副作用。它也可以用来代替伪程序设计语言来指定算法。
2020-07-06 cs.PL cs.SE
Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs
差分约束在文献中已被用于终止分析，其中它们表示形式为x' <= y + c的关系不等式，并且描述当前状态中x的值至多是前一状态中y的值加上某个整数常数c。在本文中，我们认为，命令式程序的复杂性通常来自计数器的增量和重置，这可以自然地建模的差异约束。本文提出了分析差分约束程序的第一个实用算法，并描述了如何将C程序抽象为差分约束程序。我们的方法有助于自动化的复杂性和（资源）约束分析领域，使自动摊销的复杂性分析的一类新的程序，并提供一个概念上简单的程序模型，涉及不变和约束分析。我们证明了我们的方法的有效性，通过一个彻底的实验比较真实世界的C代码：我们的工具Loopus计算的复杂性相当多的功能，在更短的时间比相关的工具从文献。
2015-08-20 cs.PL
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
Towards Patterns for Heaps and Imperative Lambdas
在函数式程序设计中，无点关系演算在程序构造的一般理论中已经取得了丰硕的成果，但对于特定的应用程序，逐点表达式可以更方便和更容易理解。在命令式编程中，精化演算已经被绑定到状态变量的逐点表达式，除了无处不在但不可见的堆。为了将点态与无点态结合起来，de Moor和Gibbons扩展了λ演算，并使用关系解释了非单射模式匹配。本文给出了该语言的一种语义，使用偏序之间的“理想关系”，以及使用谓词Transformers的第二种语义。第二种语义的动机是它与分离代数的潜在用途，用于作用于堆的程序中的模式匹配。在这些模型中，包括松弛贝塔和埃塔法律证明，并提出了一些开放的问题。
2015-10-19 cs.PL
Leroy: Library Learning for Imperative Programming Languages
本研究提出Leroy系统，通过AST转换结合Stitch框架将库学习拓展至命令式语言，经Python子集验证可实现1.04倍代码压缩并能裁剪无效抽象，提升了代码可复用性与维护性。
2024-10-09 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
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
Kyoto University（京都大学）；The University of Tokyo（东京大学）
该研究提出ConSORT类型系统，结合精化类型与分数所有权类型，解决命令式程序中别名导致的强更新判定难题，实现自动推理工具，可验证含数据结构的非平凡程序。
2026-08-11 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
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
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
A Linear First-Order Functional Intermediate Language for Verified Compilers
我们提出了线性一阶中间语言IL验证编译器。IL是一种函数式语言，可以调用非确定性环境。我们给IL条款的第二个，命令式语义解释，并获得一个寄存器转移语言。对于命令式解释，我们建立了活变量的概念。基于活变量，我们制定了一个可判定的属性称为一致性，确保功能和命令的解释一个术语相吻合。我们制定了一个寄存器分配算法的IL，并证明其正确性。该算法将一个函数式IL程序转换为一个等价的命令式IL程序。正确性来自于这样一个事实，即算法在一致地重命名局部变量后达到了一个连贯的程序。我们证明了初始程序中的最大活变量数限制了最终相干程序中不同变量的数量。整个开发都在Coq中正式化。
2015-06-04 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
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
Automating Proofs of Data-Structure Properties in Imperative Programs
我们考虑动态操作数据结构的自动推理问题。最先进的方法仅限于展开和匹配（U+M）范式，其中谓词在被视为未解释之前通过从其定义中导出的（解）折叠操作进行转换。然而，验证具有迭代循环和多个函数调用的程序的证明义务通常不会屈服于这种范式。我们的贡献是一个证明方法-超越U+M -执行自动公式重写处理以前遇到的义务，在每个证明路径作为可能的归纳假设。这使我们第一次能够系统地推理出实际方案核查所产生的各种义务。我们展示了我们的证明规则的力量，常用的引理，从而关闭现有的国家的最先进的系统中剩余的差距。另一个影响，可能更重要的是，我们的方法重新获得了组合推理的能力，并表明使用用户提供的引理不再需要现有的基准集。这不仅消除了提出适当引理的负担，而且还显著地提高了验证过程，因为引理应用与展开相结合，通常会导致非常大的搜索空间。
2014-07-23 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
Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)
针对高阶命令式程序中现有两阶段规范机制精度不足的问题，本文提出支持多阶段的 Hoare 逻辑扩展，并开发了自动化高阶验证器 Heifer，以更精确地刻画未知函数参数和递归行为。
2024-07-02 cs.PL
Optimism in Equality Saturation
University of California, Berkeley（加州大学伯克利分校）
本文提出了一种乐观的等价类分析算法，通过解决等价图表示中的微妙问题，提升了等价饱和过程的精度与效率。
2026-04-16 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
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
Circular Programs and Self-Referential Structures
本文介绍利用循环程序和自引用结构在函数式语言中实现循环链表、双向链表、线索树和队列，并通过避免中间临时结构提升空间效率。
2024-03-04 cs.PL
Semantics-Guided Synthesis
本文提出了一种新的程序合成框架，称为语义引导合成（SemGuS），它允许用户提供语法和语义的语言中的结构。SemGuS接受递归定义的大步语义，这允许它用于指定和解决命令式程序设计语言上的合成问题，该命令式编程语言可能包含具有无限行为的循环。SemGuS的可定制性质还允许在非标准语义（例如抽象语义）上定义合成问题。除了SemGuS框架，我们开发了一种算法，用于解决SemGuS问题，能够合成程序和证明不可实现性，通过编码SemGuS问题作为一个证明搜索约束角子句：特别是，我们的方法是第一个，我们知道，可以证明不可实现性的合成问题，涉及的强制性程序与无界循环，在一个无限的语法搜索空间。我们在一个名为MESSY的工具中实现了该技术，并将其应用于两个SyGuS问题（即，在表达式上）和在命令式程序设计语言上的合成问题。
2020-11-11 cs.PL
Equality Saturation: A New Approach to Optimization
传统编译器中的优化是顺序应用的，每个优化都破坏性地修改程序以产生转换后的程序，然后将其传递到下一个优化。我们提出了一种新的方法来构造编译器的优化阶段。在我们的方法中，优化采用相等分析的形式，将相等信息添加到公共中间表示中。优化器通过重复应用这些分析来推断程序片段之间的等价性，从而使中间表示充满等式。一旦饱和，中间表示编码输入程序的多个优化版本。在这一点上，盈利性启发式从饱和表示中表示的各种程序中挑选最终优化的程序。我们提出的结构优化器的方法比以前的方法有各种好处：我们的方法避免了需要担心优化排序，使使用一个全局优化启发式，选择完全优化的程序，并可用于执行翻译验证，即使在编译器比我们自己的。我们提出了我们的方法，形式化，并描述了我们选择的中间表示。我们还提出了实验结果表明，我们的方法是实用的时间和空间开销方面，是有效的发现复杂的优化机会，并有效地执行翻译验证一个现实的优化。
2011-03-25 cs.PL
Tackling the Awkward Squad for Reactive Programming: The Actor-Reactor Model
针对响应式编程在真实应用中难以处理长时间计算、副作用及命令式与响应式代码协调的问题，提出 Actor-Reactor 模型，通过严格分离与数据流组合，在 Stella 语言中实现验证。
2023-06-21 cs.PL
ImpNet: Programming Software-Defied Networks Using Imperative Techniques
软件和硬件组件是现代网络的基本组成部分。但软件组件是典型的封闭式和面向功能的。因此，很难修改这些组件。这严重影响了网络创新。此外，这导致网络策略具有用户不友好的复杂接口，并因此导致网络的物理交换机上的巨大且复杂的流表。这在许多情况下会大大降低网络性能。软件定义网络（SDN）是一种现代网络架构，可以克服上述问题。SDN的思想是向网络添加控制器设备，该控制器设备管理网络上的所有其他设备，包括网络的物理交换机。管理过程的主要任务之一是交换机学习;通过对网络的物理交换机进行编程来实现，通过向交换机（更具体地说，向交换机的流表）添加或从交换机（更具体地说，从交换机的流表）移除用于分组处理的规则。本文提出了一种高级命令式网络程序设计语言--ImpNet。ImpNet允许编写高效，但简单，功能强大的程序在控制器上运行，以控制所有其他网络设备，包括交换机。ImpNet是组合的，结构简单，富有表现力，更重要的是命令式的。介绍了ImpNet的语法以及ImpNet合同的两种操作语义。所提出的语义是静态和动态类型。两个现代应用程序编程使用ImpNet的文件中显示。文中还给出了应用程序的语义。
2014-07-08 cs.NI cs.PL
Efficient compilation and execution of synchronous programs via type-state programming
针对同步程序编译中状态空间爆炸导致难生成高效可执行文件的问题，提出基于图重写规则的线性时间编译技术，结合C++模板元编程生成类型状态程序，实现了与现有水平相当的编译效率和二进制体积，执行速度提升31%-60%。
2025-08-02 cs.PL
Sketch-Guided Equality Saturation: Scaling Equality Saturation to Complex Optimizations of Functional Programs
为不同的硬件和应用程序域生成高性能代码是一项挑战。带有map和reduce等模式的函数数组程序设计语言已经成功地与项重写结合起来，以定义和探索优化空间。然而，决定应用什么顺序的重写是困难的，并且对重写后的程序的性能有巨大的影响。相等饱和通过探索许多可能的方法来应用重写来避免这个问题，有效地在e图数据结构中表示许多等效程序。当重写函数语言术语时，等式饱和有一些限制，因为当前使用的是λ演算的朴素编码。我们提出了新的技术编码多态类型的lambda演算，并表明，有效的编码减少了运行时间和内存消耗的数量级的平等饱和。此外，等式饱和还不能扩展到复杂的编译器优化。这些从数千个重写步骤的长重写序列中出现，并且可能使用导致e图快速增长过大的重写规则的病态组合。本文介绍了\emph{sketch-guided equality saturation}，一种允许程序员提供程序草图以指导重写的半自动技术。草图引导的等式饱和度评估了七个复杂的矩阵乘法优化，包括循环阻塞，矢量化和多线程。即使使用高效的λ演算编码，无指导的等式饱和也只能定位这些优化中最简单的两个，剩下的五个即使用一个小时的编译时间和60 GB的RAM也无法发现。通过指定三个或更少的草图指南，所有七个优化都可以在几秒钟的编译时间内找到，使用不到1GB的RAM，并生成高性能代码。
2022-06-03 cs.PF cs.PL
eqsat: An Equality Saturation Dialect for Non-destructive Rewriting
本文提出 MLIR 方言 eqsat，将 e-graph 与等饱和原生嵌入编译器 IR，以支持贯穿编译流程的非破坏性构造性重写并复用现有 MLIR 优化遍。
2025-05-15 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
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
Natural Hoare Logic: Towards formal verification of programs from logical forms of natural language specifications
形式化验证为软件的正确性提供了强有力的保证，这在安全或安全关键系统中尤为重要。霍尔逻辑是一种广泛使用的形式主义，用于以前置条件/后置条件断言的形式针对规范对软件进行严格验证。语义解析技术的进步和更高的计算能力使我们能够从自然语言文本中提取语义内容作为形式逻辑形式，具有越来越高的准确性和覆盖率。本文提出了一个基于霍尔逻辑的命令式程序形式化验证的形式化框架，该框架使用由自然语言断言的组合语义解析生成的逻辑形式。我们称这种推理方法为自然霍尔逻辑。这使得能够直接针对领域专家以自然语言指定的安全需求对软件进行形式化验证。我们认为这两个声明性断言的程序不变量和状态变化以及命令性断言，指定命令改变程序状态。我们将讨论如何推理方法可以扩展使用领域知识和实用的方法，防止语义分析器错误。
2021-03-04 cs.PL
Latent Idiom Recognition for a Minimalist Functional Array Language using Equality Saturation
本文提出用极简函数式数组语言结合等式饱和自动识别代码惯用法，匹配BLAS和PyTorch核心函数，实现1.46倍几何平均加速。
2023-12-29 cs.PL
Semantic foundations of equality saturation
本文为等式饱和技术建立了基于树自动机的不动点语义，揭示其与chase的深层联系，并研究了不同实例情形下的终止性复杂度，提出基于无环性的终止性句法准则。
2025-01-05 cs.DB 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
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
A Semantics for Probabilistic Control-Flow Graphs
本文提出了一种新的操作语义的概率控制流图（pCFG）的概率命令式程序与随机分配和“观察”（或条件）语句。当控制从pCFG中的一个节点移动到另一个节点时，语义转换概率分布（在商店上）。我们将此语义的标准，预期转换，指称语义的结构化概率命令式程序，结构化程序翻译成（非结构化）pCFGs，并证明充分的翻译。这表明操作语义可以在不丢失信息的情况下使用，并且忠实于“预期”语义，因此可以用于推理，例如，转换的正确性（正如我们在配套文章中所做的那样）。
2017-11-07 cs.PL
WaveCert: Translation Validation for Asynchronous Dataflow Programs via Dynamic Fractional Permissions
针对数据流编译器转换异步程序易出错的问题，提出基于动态分数权限的翻译验证技术WaveCert，在RipTide CGRA架构的编译器中发现8个漏洞并验证了基准套件程序的编译正确性。
2024-04-12 cs.AR cs.PL
Scaling Program Synthesis Based Technology Mapping with Equality Saturation
本文提出Churchroad技术映射器，将等价饱和与程序综合工具结合，解决FPGA映射中草图编写困难及SMT求解器乘法处理弱的问题，可处理更大更复杂的设计且无需用户提供草图。
2024-11-19 cs.AR cs.PL
Associativity and Commutativity in Equality Saturation
Saarland University（萨尔兰大学）
本文针对等式饱和中 e-graph 指数增长问题，提出通过多重集合存储项以原生处理结合性与交换性运算符的扩展，初步证明可渐近减少内存使用。
2026-10-02 cs.PL
The While language
本文给出了一种简单的命令式程序设计语言的形式化。目标是研究和开发“动手”的程序设计语言的形式规范，即它的语法，操作语义和类型系统。为了获得该语言的可执行版本，我们在Racket中实现了它的操作语义和类型系统。
2016-04-12 cs.PL
Abstract interpretation as anti-refinement
本文展示了命令式程序的抽象解释和精化演算之间的对应关系：在精化演算中，程序的抽象解释是一个规范，它是一个函数。这种对应关系可以用来指导设计机械验证的静态分析，保持正确性证明以及分离的启发式部分的算法。
2014-06-13 cs.PL
On Termination of Polynomial Programs with Equality Conditions
研究了一类多路多项式规划的终止问题，其中对程序变量的所有赋值都是多项式，循环和条件语句的测试条件都是多项式等式.我们表明，这样的程序的非终止输入（NTI）的集合是算法可计算的，从而导致其终止的可判定性。据我们所知，所考虑的MPP家族是迄今为止可决定终止的最大家族。本文给出了一个显式的递归函数，它本质上是阿克曼的，用来计算多项式理想在控制函数下的升链的最大长度，从而得到了Seidenberg问题的完整答案.这个最大的长度有利于我们的算法计算NTI和决定终止MPP的精确的复杂性分析。我们扩展我们的方法与多项式守护命令的程序，并显示如何不完整的程序与不等式警卫的MPP可以得到。我们的技术的多项式程序的不变生成的应用。
2020-09-01 cs.PL cs.SC
A Model of Cooperative Threads
我们开发了一个模型的并发命令式编程线程。我们专注于一个小的命令式语言与合作的线程，执行无中断，直到他们终止或显式地产生控制。我们定义并研究了这种语言的基于跟踪的指称语义，这种语义是完全抽象的，但数学上是初等的。我们还给出了一个方程理论的计算效果，基础的语言，包括线程产卵。然后，我们分析线程的自由代数单子这个理论。
2010-10-20 cs.PL
Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
最近的程序合成技术帮助用户定制CAD模型（例如，用于3D打印），将低级三角形网格反编译为构造性实体几何（CSG）表达式。如果没有循环或函数，编辑CSG可能需要许多协调的更改，并且现有的网格反编译器使用可能混淆高级结构的语法。本文提出了第二个反编译阶段，强大的“收缩”非结构化CSG表达式到更多的可编辑程序与地图和折叠操作。我们提出Szalinski，一个工具，使用平等饱和与语义保持CAD重写有效地搜索较小的等效程序。Szalinski依赖于逆变换，这是求解器推测性地将等价物添加到E图的一种新方法。我们定性评估Szalinski的案例研究，显示它如何与现有的网格反编译器组成，并证明Szalinski可以在几秒钟内缩小大型模型。
2020-04-12 cs.CG 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
