PEQcheck: Localized and Context-aware Checking of Functional Equivalence (Technical Report)
重构不得改变程序的功能。然而，并不是所有的重构都满足这个要求。因此，必须明确检查重构不会改变功能。由于很少有一个正式的规格说明程序的行为，我们利用原来的程序作为功能规范。然后，我们检查原始程序和重构后的程序在功能上是否等价。为此，我们采用一个共同的想法，减少等价性检查程序验证。为了提高效率，我们的等价性检查PEQcheck构造一个验证任务，每个重构的代码段，而不是一个功能，通常由以前的工作。此外，PEQcheck考虑代码段的上下文。例如，只有被修改的和活的变量才需要是等效的，只读变量可以在原始代码段和重构的代码段之间共享。此外，我们的评估证明，本地化和上下文感知检查执行的\peqcheck确实可以是有益的。
2021-03-22 cs.LO cs.PL
Program Equivalence for Assisted Grading of Functional Programs (Extended Version)
在涉及编程作业的课程中，给学生有意义的反馈是一个重要的挑战。人类可以通过手动评分程序来提供有用的反馈，但这是一个耗时，劳动密集型，并且通常无聊的过程。自动评分器速度快，可扩展性好，但它们通常提供的反馈很差。虽然已经有关于改进自动分级机的研究，但是关于缩放和改进人类分级的研究是有限的。我们建议通过使用等价算法来增强手动评分过程，该算法可以识别学生提交文件之间的等价关系，从而扩展人工评分。这使人类评分员能够一次为多个学生提交的内容提供有针对性的反馈。我们的技术在两个方面是保守的。首先，它识别算法相似的提交之间的等效性，例如，它不能识别快速排序和合并排序之间的等价性。其次，它使用正式的方法，而不是聚类算法从机器学习文献。这使我们能够证明一个可靠的结果，保证提交永远不会错误地聚集在一起。尽管只有报告等价时，有算法的相似性和正式证明等价的能力，我们表明，我们的技术可以显着减少评分时间从介绍函数编程课程的数千个编程提交。
2020-10-15 cs.PL
On Propositional Program Equivalence (extended abstract)
本文从带保护的Kleene代数与测试的视角，讨论命题程序等价性的最新进展，该等价性在抽象语句语义后可判定且实践可行。
2025-07-10 cs.PL
Program Equivalence in an Untyped, Call-by-value Lambda Calculus with Uncurried Recursive Functions
我们的目标是推理Erlang程序的行为保持转换的正确性。行为保留的特点是语义等价。基于我们现有的形式语义的核心Erlang，我们调查合适的等价关系的潜在定义。特别是，我们适应了一些现有的表达等价的方法，一个简单的功能程序设计语言，进行顺序核心Erlang的主要特点，然后我们检查的等价关系的属性，并正式建立它们之间的连接。本文的结果，包括所有定理及其证明，已使用Coq证明助手进行了机器检查。
2022-08-30 cs.PL
Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence
本文提出 PDNF 互模拟，利用无栈 LTS、调用栈即时饱和与 up-to 技术，使具有局部状态的高阶程序在无界栈和未知函数输入下仍可判定上下文等价性。
2023-11-02 cs.LO cs.PL
Towards a constraint solver for proving confluence with invariant and equivalence of realistic CHR programs
一个不确定性程序的汇流确保了功能性的输入输出关系，使程序员不必考虑实际的调度策略，并允许优化和并行实现。汇流模等价的更一般的性质确保等价的输入与等价的输出相关，而不需要是相同的。不变量下的合流也被认为是。约束处理规则是基于重写的逻辑程序设计语言的一个重要例子，本文旨在给出一种可机械化的方法来证明终止程序的汇流模等价性。虽然早期的方法，融合的可编程逻辑程序关注一个理想化的逻辑子集，我们指的是一个语义与标准的基于Prolog的实现兼容。我们指定了一个元级约束语言，在其中不变量和等价可以表示和操纵，扩展我们以前的理论结果走向实际的实施。
2018-09-13 cs.PL
Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Systems
我们调查程序等价的线性高阶（顺序）语言赋予计算效果的原语。更具体地说，我们研究了基于操作的概念的程序等价的线性$λ$ -演算明确复制和代数效果\emph{à la} Plotkin和电源。这样的演算明确了复制和线性之间的相互作用，这是计算的内涵方面，而效果是\emph{extensional}。我们回顾了一些文献中提出的线性结石等价的概念，并显示其局限性时，适用于有效的结石复制是一等公民。然后，我们引入资源转换系统，即转换系统的状态是建立在元组的程序表示可用的资源，作为一个操作语义会计程序的内涵和外延的交互行为。我们的主要结果是一个健全的和完整的表征上下文等价的跟踪等价定义的资源转移系统。
2021-06-24 cs.LO cs.PL
Completely Automated Equivalence Proofs
不完全的（即，终止不敏感）等价在软件开发和教育中具有重要的实际应用。传统的等价验证器通常依赖于给定的关系摘要和建议的同步点的组合;对于没有正式方法背景的程序员来说，这样的信息可能非常困难，以提供具有不同逻辑的程序对。在这项工作中，我们提出了一个完全自动化的验证确定部分等价，命名为Pequod。Pequod自动合成传统上只能通过仔细手动构造产品程序才能实现的表达性等价证明。为此，Pequod为选定的程序路径对合成关系证明，并将每个路径的关系证明组合起来，以合成关系程序不变量。为了评估Pequod，我们将其实现为针对Java虚拟机字节码的工具，并将其应用于验证学生提交的数百对解决方案的等效性，这些解决方案用于流行的在线编码平台上托管的问题，其中大部分无法通过现有技术进行验证。
2017-05-08 cs.PL
Semantical Equivalence of the Control Flow Graph and the Program Dependence Graph
程序依赖图（PDG）表示程序中语句之间的数据和控制依赖。本文提出了程序依赖图的操作语义。由于PDG排除了驻留在顺序程序中的语句的人为顺序，因此PDG的执行不是唯一的。然而，我们确定了一类具有唯一最终执行状态的PDG，称为确定性PDG。我们证明了控制流图的操作语义等价于确定性PDG的操作语义。确定性PDG的类适当地包括从结构良好的程序获得的PDG。因此，我们的操作语义的PDG是更一般的PDG结构良好的程序，这是已经建立在文献中。
2018-03-08 cs.PL
Equivalence and Similarity Refutation for Probabilistic Programs
本文提出一种全自动的静态方法，通过同时计算输出函数、上期望上鞅和下期望下鞅来反驳无限状态概率程序的等价性与相似性，并提供形式化正确性保证。
2024-04-04 cs.FL cs.PL
A fix-point characterization of Herbrand equivalence of expressions in data flow frameworks
确定数据流框架中每个程序点上的Herbrand等价项是程序分析中的一个核心问题。在数据流框架中，大多数用于计算Herbrand等价的著名算法通过在与给定流图相关的一些短表达式的抽象格上进行迭代不动点计算来进行。然而，Herbrand等价的数学定义是基于所有可能表达式的（无限）集合上的所有路径特征的满足。本文的目的是发展一个格理论的不动点公式的Herbrand等价的（无限）具体格上定义的所有条款可构造的变量，常数和运营商的程序。目前的表征使用的概念，Herbrand同余的公理化配方，并定义了（无限）具体格Herbrand同余。传递函数和非确定性分配制定为单调函数在这个具体的晶格。Herbrand等价被定义为在上述具体格的适当乘积格上定义的复合传递函数的最大不动点。在上述格理论框架下，给出了Herbrand等价的经典遍路相交定义的一个新形式，并证明了其等价于新的格理论不动点刻画.
2017-10-20 cs.LO cs.PL
Contextual Equivalence for Signal Flow Graphs
我们扩展了信号流演算-经典的信号流图计算模型的组成帐户-包括仿射行为，并提供了一个新的操作语义。增加的表达能力，使我们能够定义一个规范的概念，上下文等价，我们表明，以符合指称平等。最后，我们将微积分的可实现片段：那些表示（仿射）信号流图计算的术语。
2020-02-20 cs.LO cs.PL
Observational equivalences for linear logic CC languages
线性逻辑并发约束规划（LCC）是并发约束规划（CC）的一种扩展，其中约束系统是基于Girard的线性逻辑而不是经典逻辑。在本文中，我们解决这个编程框架的程序等价性问题。为了这个目的，我们提出了一个结构化的操作语义LCC的标签转换系统的基础上，并调查不同的概念的观察等价的启发，最先进的进程代数。然后，我们证明了异步π演算可以被看作是LCC的简单的语法限制。最后，我们表明LCC观测等价可以直接转置到经典的并发约束语言和约束处理规则，并调查由此产生的等价。
2011-08-01 cs.PL
Hashing Modulo Context-Sensitive $α$-Equivalence
针对传统α-等价比较上下文子项的不足，提出上下文敏感α-等价概念并证明其与互模拟等价一致，设计O(n log n)哈希方案优化此前时间界，可用于构建机器学习用的大规模数学知识图。
2024-06-23 cs.LO cs.PL
Irene: Equivalence Checking of Hybrid Quantum Programs via Structure-Preserving Symbolic Reduction
Shanghai Jiao Tong University（上海交通大学）
提出Irene框架，通过保结构符号化简在门级、混合路径和及密度核三个层次验证混合量子程序等价性，在1982个程序对中解决79.92%，并发现15个编译器缺陷。
2026-09-30 cs.LO cs.PL cs.SE
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
本文提出高阶近似关系分离逻辑 Approxis，通过误差信用支持概率高阶有状态程序的近似与精确等价推理，并在 Coq/Iris 中机械化验证安全与采样示例。
2024-12-03 cs.LO cs.PL
Interaction Equivalence
本文在无类型λ演算中提出交互等价性，通过只观察项与上下文的交互步数而忽略内部步骤，证明其构成等式理论并首次在不增强上下文区分能力的情况下观察性刻画了Böhm树相等理论B。
2024-11-25 cs.LO cs.PL
Coarser Equivalences for Causal Concurrency
本文研究并发程序运行中迹等价的松弛问题，提出了一种基于粒交换性的新等价关系“粒等价”，在比迹等价更松弛的同时，保持了在常数空间内判定因果并发性的算法优势。
2023-10-26 cs.FL cs.LO cs.PL
Proving Functional Program Equivalence via Directed Lemma Synthesis
针对结构归纳法不足以证明函数式程序等价性的问题，本文提出定向引理合成方法，将引理合成归约为特殊程序合成问题，相比现有最优方法大幅缩短运行时间并解决更多任务。
2024-05-19 cs.PL
Probabilistic Program Equivalence for NetKAT
我们解决的问题，决定是否两个概率程序是等价的概率NetKAT，一种形式语言，用于指定和推理的分组交换网络的行为。我们表明，这个问题是可判定的历史自由片段的语言开发一个有效的决策过程的基础上随机矩阵。主要的挑战在于推理迭代，我们通过设计一个编码的程序语义作为一个有限状态吸收马尔可夫链，其极限分布可以精确计算。在一个真实世界的数据中心网络的扩展案例研究中，我们通过分析马尔可夫链语义自动验证了各种感兴趣的定量属性，包括故障情况下的弹性。
2018-03-24 cs.PL
Refuting Equivalence in Probabilistic Programs with Conditioning
针对带 observe 与 score 的概率程序，本文提出基于 weighted restarting 变换的等价性反驳方法，可全自动给出可证明正确的不等价判定。
2025-01-11 cs.FL cs.PL
Context-Free Session Types for Applied Pi-Calculus
我们提出了一个二进制会话类型系统，使用上下文无关的会话类型的一个版本的应用π演算的阿巴迪等。al.，其中只能发送基本项、常量和通道。会话类型类似于BPA的过程术语，我们使用互模拟等价来表征类型等价。我们提出了一个定义在类型等价类上的约束类型系统，其中类型等价被构建到类型系统中。这两种类型的系统满足一般的健全性属性，这是建立一个呼吁通用会话类型系统的PSI演算。
2018-08-27 cs.LO cs.PL
Sheaf-Cohomological Program Analysis: Unifying Bug Finding, Equivalence, and Verification via Čech Cohomology
Microsoft Research（微软研究院）
本文提出通过Čech上同调统一程序分析中的类型检查、Bug查找和等价性验证，利用上同调群H^0和H^1解决类型错误和等价性失败问题，并在Deppy工具中验证了其有效性。
2026-03-27 cs.PL
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
本文提出在 F* 中用单子表示效应程序并复用纯程序推理能力的统一关系验证框架，支持信息流控制、高阶等价与精化、优化正确性及博弈密码安全等分析。
2019-10-12 cs.CR cs.PL
Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules
Colorado State University（科罗拉多州立大学）；KTH Royal Institute of Technology（瑞典皇家理工学院）
本文提出基于transformer的S4Eq系统，通过自监督样本选择增量训练生成重写规则序列，自动证明直线程序对的语义等价性，在10,000对程序上达到97%证明成功率。
2023-07-09 cs.LG cs.PL
Analyzing Graph Transformation Systems through Constraint Handling Rules
图转换系统和约束处理规则是基于规则的非确定性状态转换系统。GTS以其强大的融合和程序等价性分析而闻名，为此，我们在这项工作中提供了将其应用于GTS的基础。我们给出了一个健全的和完整的嵌入GTS的可移植性，研究了一个嵌入的GTS的融合，并提供了一个程序等价性分析GTS通过嵌入。结果证实了适用的CHR为基础的程序分析嵌入在CHR的其他形式主义。
2010-06-15 cs.LO cs.PL
Higher-order Context-free Session Types in System F
我们提出了一个扩展的系统F与高阶上下文无关的会话类型。功能类型与会话类型的混合已经被证明是类型等价形式化的一个挑战：而功能类型等价通常是基于规则的，会话类型等价通常遵循基于互模拟的语义方法。我们提出了一个统一的方法，处理功能和会话类型的等价性在一起。我们提出了三个概念的类型等价：基于语法规则的版本，语义bisimulation-based版本，和算法版本减少到简单的语法的互模拟的问题。我们证明了这三个概念相吻合，并得出一个可判定性结果的类型等价问题的高阶上下文无关的会话类型。
2022-03-24 cs.FL cs.LO cs.PL
Dynamic Verification with Observational Equivalence of C/C++ Concurrency
松弛内存模型（rmm）语义下的程序执行更难分析; rmm语义导致程序事件的乱序执行，导致状态空间爆炸。动态偏序约简（DPOR）是一种解决这种状态空间爆炸的强大技术，已被用于验证RMM下的程序，如TSO，PSO和POWER。这种DPOR技术的核心是跟踪等价的概念，它是基于程序事件之间的独立关系计算的。我们提出了一个粗糙的概念，称为观测等价（OE）的RMM感知跟踪等价。如果每个读事件在两个行为中读取相同的值，则两个程序行为在观察上是等效的。我们提出了一个概念的观测独立性（OI），并提供了一个算法的建设，以计算迹等价（模OI）有效。我们还证明了DPOR与OE线程C/C++程序的有效性，首先提供了一个精心制作的happensbefore（HB）的关系捕捉C/C++并发语义。我们实现了一个运行时模型检查称为Drista的技术。我们的实验表明，（i）与现有的nonOE技术相比，我们实现了显着节省的跟踪下探索OE的数量，（ii）我们的治疗C/C++并发性比现有的国家的最先进的技术更广泛。
2022-07-30 cs.DC cs.PL
Metric Program Synthesis
我们提出了一种新的域不可知的合成技术，从输入输出的例子生成程序。我们的方法，称为度量程序合成，放宽了众所周知的观测等价性的想法（广泛用于自下而上枚举合成）到一个较弱的观测相似性的概念，减少合成器需要探索的搜索空间的目标。我们的方法聚类程序到等价类的距离度量的基础上，并构造一个版本空间，competencies表示“近似正确”的程序。然后，给定一个“足够接近”的程序从这个版本空间采样，我们的方法使用的距离引导修复算法找到一个程序，完全匹配给定的输入输出的例子。我们已经实现了我们提出的度量程序合成技术中的一个工具，称为SyMetric和评估它在三个不同的领域考虑在以前的工作。我们的评估表明，SyMetric优于其他使用观测等效性的领域不可知合成器，并且它实现了与针对这些领域设计或训练的特定领域合成器竞争的结果。
2022-10-10 cs.PL
LLMs are Brittle to Simple Code Transformations: Introducing CETBench - A Benchmark for Code-Equivalence Checking
Indian Institute of Technology Delhi（印度理工学院德里分校）；IBM Research AI（IBM研究院）
本文提出CETBench基准，通过对程序对施加随机代码变换生成等价性检查数据，发现简单变换即可显著降低SOTA LLMs的性能，并提出基于微调的方法加以改进，揭示LLMs在代码语义理解上仍存在明显不足。
2026-10-21 cs.CL cs.LG cs.PL
Recursive Session Logical Relations
程序等价是程序性质推理和证明的支点。对于不干扰，例如，程序等价的保密水平的观察员。逻辑关系是这种证明的有力推动者。逻辑关系直到最近才被用于会话类型--但仅用于终止语言。本文将逻辑关系扩展到递归会话类型。它为线性会话类型的进度敏感非干扰开发了一个逻辑关系，解决了非终止和并发带来的挑战。这些贡献包括安全多态过程和与元理论的逻辑关系。一个显着的特点是选择的“步骤指数”的逻辑关系，允许传递性和可靠性的自然证明。
2022-08-30 cs.LO cs.PL
Kleene Algebra with Tests and Coq Tools for While Programs
我们提出了一个Coq库Kleene代数与测试，包括证明他们的完整性在适当的概念的语言，他们的方程理论的决策程序，并利用在这样的理论的一个特定形状的假设的工具。带有测试的Kleene代数使得在大多数命令式程序设计语言中表示if-then-else语句和while循环成为可能。它们实际上是由Kozen引入的，作为命题霍尔逻辑的替代。我们展示了如何利用相应的Coq工具的程序验证的上下文中证明等价的，而程序，正确的一些标准的编译器优化，霍尔规则的部分正确性，以及一个特别具有挑战性的等价流程图计划。
2013-02-07 cs.LO cs.MS cs.PL
A Programming Language for Feasible Solutions
Shanghai Jiao Tong University（上海交通大学）
本文提出一种新的 imperative 编程语言，其静态类型系统确保所有可定义程序在多项式时间内运行，同时所有多项式时间可解问题均可由该语言程序解决。理论和实践上均具有创新性。
2026-04-03 cs.PL
On Feller Continuity and Full Abstraction (Long Version)
我们研究了应用双相似性的性质在$λ$ -演算赋予运营商从连续分布的采样。一方面，我们表明，双相似性，逻辑等价，测试等价都符合上下文等价时，实数只能通过连续函数进行操作。实现这一结果的关键因素是一个新的概念，标记马尔可夫过程，我们相信独立的利益，是一个广泛的一类LMP的共归纳和逻辑启发的等价物相吻合的费勒连续性。另一方面，我们表明，如果没有限制的方式实数被操纵，表征上下文等价原来是困难的，大多数上述概念的等价甚至是不健全的。
2022-07-21 cs.LO cs.PL
Proving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Models
Position1 Department1 Institution1 Street1 Address1 City1 State1 Post-Code1 Country1；Position2a Department2a Institution2a Street2a Address2a City2a State2a Post-Code2a Country2a；Position2b Department2b Institution2b Street3b Address2b City2b State2b Post-Code2b Country2b
我们的目标是可证明计算两个复杂的表达式树之间的等价性的问题。为此，我们形式化的问题，两个这样的程序之间的等价性，找到一组语义保持重写规则从一个到另一个，这样，重写后的两个程序在结构上是相同的，因此平凡equivalent. Then，我们开发了一个图形序列神经网络系统的程序等价性，训练产生这样的重写序列从一个精心制作的自动示例生成算法。我们广泛评估我们的系统上丰富的多类型线性代数表达式语言，使用任意组合的100+图形重写公理的等价。我们的机器学习系统保证所有真阴性的正确性，并通过设计确保零误报。它通过推理为10，000个隔离测试的等价表达式对中的93%输出有效的等价性证明，使用多达50个术语表达式。在所有情况下，序列的有效性产生，因此程序等价性的可证明断言总是可计算的，在可忽略的时间。
2021-06-09 cs.LG cs.PL
ScratchLens: Lens-Parametric Behavioral Equivalence for Scratch Programs
University of Waterloo（滑铁卢大学）
针对块编程语言中程序等价性判定问题，提出透镜参数化等价框架SPECTRA，通过因果IR、规范化和Mazurkiewicz迹商等技术，实现高精度行为等价判定。
2026-06-17 cs.PL cs.SE
Contextual equivalence for higher-order pi-calculus revisited
高阶pi演算是pi演算的扩展，允许进程抽象的通信，而不仅仅是名称。Sangiorgi在他的论文中深入研究了高阶π演算的上下文等价性，使用标记的过渡系统和正常的互模拟。不幸的是，这里使用的证明技术需要限制语言只允许有限类型。我们重新审视这种演算，并提供了一种替代的介绍标记的过渡系统和一种新的证明技术，使我们能够提供一个完全抽象的上下文等价的特性，使用标记的过渡和互模拟高阶π演算递归类型也。
2006-01-24 cs.PL
Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion
我们提出了一个完整的推理原则，上下文等价的非类型化概率语言。该语言包括连续（实值）随机变量，条件和评分。它还包括递归，因为标准的按值调用定点组合子是可表达的。我们证明了几个等价模式，包括熟悉的事实，从λ演算以及特定的概率编程的结果，我们的表征的可用性。特别是，我们用它来证明，重新排序的随机抽取概率程序保持上下文等价。例如，这使我们能够证明，（let x = $e_1$ in let y = $e_2$ in $e_0$）等价于（let y = $e_2$ in let x = $e_1$ in $e_0$）（假设$x$在$e_2$中不游离，$y$在$e_1$中不游离），尽管$e_1$和$e_2$可能具有采样和评分效应。
2018-07-08 cs.PL
The Output-Space Hypothesis: Enumerative Equivalence Checking for Tensor Programs
University of Pennsylvania（宾夕法尼亚大学）
提出输出空间假设，通过翻转量词检查单个输出位置对所有输入的等价性，实现张量程序更一致的错误发现，在6988个AI编写的CUDA内核中找出600个隐藏错误。
2026-09-18 cs.LG cs.PL cs.SE
Faultless: A Program Equivalence Technique for Validating and Evaluating Neural Decompilers
Carnegie Mellon University（卡内基梅隆大学）；Carnegie Mellon University Software Engineering Institute（卡内基梅隆大学软件工程研究所）
针对神经反编译器输出不可信问题，提出Faultless程序等价性技术，通过静态符号执行比较确定性反编译与神经反编译结果，实现翻译验证和模型评估。
2026-09-29 cs.CR cs.PL cs.SE
Quantitative Symbolic Patch Impact Analysis
University of California, Santa Barbara（加州大学圣塔芭芭拉分校）
本文提出量化部分等价分析方法，用于评估软件补丁行为差异，通过符号分析识别输入条件下的等价或非等价行为，量化补丁影响。
2026-05-11 cs.PL cs.SE
EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking
Stanford University（斯坦福大学）；MIT（麻省理工学院）；Google（谷歌）；Nanjing University（南京大学）；Intel（英特尔）
本文提出 EquiBench 基准，通过等价性检查评估大语言模型对程序语义的推理能力，发现现有模型在困难类别上仅略优于随机基线，且多依赖语法相似性而非真正的语义推理。
2025-09-19 cs.AI cs.CL cs.LG
A Classical Realizability Model for a Semantical Value Restriction
我们提出了一个新的类型系统，支持程序的证明，在一个呼叫的值的语言与控制运营商。证明机制依赖于（非类型化）程序的观察等价性。它出现在两个类型构造函数中，用于指定程序属性和编码依赖产品。主要的挑战来自于由于价值限制而导致的依赖性产品缺乏表现力。为了规避这个限制，我们放松了语法限制，只要求等价于一个值。通过构建一个经典的可实现性模型，在三个层次（值，堆栈和条款）的语义上获得的系统的一致性。
2016-04-07 cs.LO cs.PL math.LO
Detecting and Explaining (In-)equivalence of Context-Free Grammars
Ruhr University Bochum（波鸿鲁尔大学）；University of Oxford（牛津大学）
本文提出了一种可扩展框架，用于决定、证明和解释上下文无关文法的等价性。通过实现该框架并在教育支持系统中收集的大型数据集上进行评估，展示了其在处理大量数据时的有效性。
2026-04-08 cs.CY cs.FL cs.PL
Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
无状态模型检验（SMC）是一种并发程序的验证技术，它通过探索所有可能的线程冲突来检查安全违规。当与动态偏序约简（DPOR）结合时，它是非常有效的，DPOR引入了一个等价类，并且在每个等价类中只需要探索一个。即使使用DPOR，SMC也经常花费不必要的努力来探索纯循环迭代，即，对程序状态没有影响。我们提出的技术，使SMC与DPOR更有效的纯循环迭代程序。第一种是静态程序分析，用于检测循环纯度和相关的程序转换，称为部分循环纯度消除，插入假设语句以阻止纯循环迭代。随后，其中一些假设被转换为await语句，完全删除了许多假设阻止的执行。最后，我们提出了一个扩展的标准DPOR等价，通过削弱事件之间的冲突关系。所有这些技术被纳入一个新的DPOR算法，最佳DPOR等待，它可以处理等待和较弱的冲突关系，是最佳的意义上，它只探索一个执行在每个等价类，也可以诊断活锁。我们在Nidhugg中的实现表明，这些技术可以显着加快并行程序的分析，这些程序目前对SMC工具来说是具有挑战性的，无论是探索其完整的交织集，还是检测其中的并发错误。
2022-08-19 cs.PL cs.SE
Hashing Modulo Alpha-Equivalence
在许多应用中，人们希望标识程序语法树的相同子树。理想情况下，这种识别应该对程序的alpha重命名具有鲁棒性，但没有现有技术显示出以良好的效率实现这一点（在表达大小上优于$\mathcal{O}(n^2)$）。我们提出了一种新的，渐近有效的方式来散列模α-等价。我们的方法的一个关键见解是使用弱（可交换）散列组合器在建设中的一个点，这承认一个算法与$\mathcal{O}(n (\log n)^2)$时间复杂度。我们证明，使用的交换组合器，但产生一个强大的哈希低碰撞概率。数值基准证明了该方法的渐近行为。
2021-05-06 cs.DS cs.PL
Equivalence Checking of Non-deterministic Operations
检查操作的语义等价性是软件开发中的一项重要任务。例如，回归测试是在开发和改进软件系统时执行的例行任务，并且软件包管理者要求在同一主版本内的包的不同版本中的操作的等效性。需要一个坚实的基础来支持这一过程的良好自动化。已经表明，当存在非确定性特征时，等价的概念并不明显。本文讨论了函数逻辑程序中等价性的一般概念，提出了一种实用的等价性检验方法，并将该方法集成到一个基于属性的测试工具中，用于软件包管理器中对软件包的语义版本进行检验。
2019-09-20 cs.PL
Soliduzz: Finding Miscompilations in Smart-Contract Compilers with Assertion-Driven Equivalence Oracles
TU Wien（维也纳工业大学）；Consensys Diligence
Soliduzz是一种用断言驱动等价预言机结合乘积程序、符号EMI等变形转换，在solc等三款EVM智能合约编译器中发现29个bug的方法。
2026-10-13 cs.PL cs.SE
Translating Xd-C programs to MSVL programs
C语言是最流行的软件系统语言之一。为了验证C语言系统的安全性、可靠性和保密性，采用了基于建模、仿真和验证语言（MSVL）及其编译器MC的代码级运行时验证工具UMC 4 M。为此，必须将C程序$P$转换为MSVL程序M，并且还将所需属性$Q$的否定转换为MSVL程序M '，然后用MC编译和执行“M和M”。通过评估是否存在新MSVL程序M和M”的可接受执行来检查$P$是否违反$Q$。因此，如何将C程序翻译成MSVL程序是一个关键问题。然而，一般来说，C是复杂的结构与goto语句。在本文中，我们将C语言的语法限制在一个合适的子集中，称为Xd-C，而不会损失表达能力。此外，我们提出了一个从Xd-C程序到MSVL程序的翻译算法的基础上的表达式和语句的翻译算法。此外，还归纳地证明了Xd-C和MSVL程序中表达式和语句的等价性。最后证明了Xd-C源程序与MSVL源程序的等价性。此外，所提出的方法已经实现了一个工具称为$C2M$。一个基准的实验，包括13个真实世界的Xd-C程序进行。结果表明，$C2M$是有效的。
2019-01-19 cs.PL
Partial Reductions for Kleene Algebra with Linear Hypotheses
LIACS, Leiden University（莱顿大学 LIACS）
研究如何为克林代数添加假设以推理程序等价性。核心方法是基于自动机的构造来推导归约。主要贡献是能机械地为广泛假设类导出归约，可实现部分完备性，自动建立更多等价性的可证性。
2026-07-07 cs.PL
