Bridging the Gap between Programming Languages and Hardware Weak Memory Models
我们开发了一种新的中间弱内存模型IMM，作为将从具有弱内存一致性语义的并发程序设计语言到主流多核架构（例如POWER和ARM）的编译正确性证明模块化的一种方式。我们使用IMM来证明编译的正确性，从Kang等人的有前途的语义到POWER（从而修正和改进他们的结果）和ARMv7，以及最近修订的ARMv 8模型。我们的结果在Coq中是机械化的，据我们所知，这些是第一个机器验证的编译正确性结果，用于比x86-TSO更弱的模型。
2018-11-09 cs.PL
Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications (Extended Version)
EPFL（洛桑联邦理工学院）；DI ENS, École Normale Supérieure, PSL, CNRS（巴黎高等师范学院计算机科学研究所，PSL大学，法国国家科学研究中心）
本文提出首个机验证的正则表达式语义，通过证明等价于ECMAScript规范，展示其在实际应用中的有效性，包括新上下文等价性概念和PikeVM算法的首次形式证明。
2026-04-07 cs.PL
Contravariant Universe Subtyping, Formalized, Mechanized
The University of Hong Kong（香港大学）；Amazon（亚马逊）
本文针对核心马丁-洛夫类型理论，在Rocq的McTT内核基础上，形式化并机械化研究反变宇宙子类型化，提出两种子类型化算法，通过互模拟关系证明其完备性，完善了类型检查器的已验证流水线。
2026-10-14 cs.PL
Bringing Iris into the Verified Software Toolchain
Verified Software Toolchain（VST）是一个使用分离逻辑证明C程序正确性的系统。通过连接到经过验证的编译器CompCert，它为我们可以编译和运行的真实C代码提供了最强的正确性保证。VST从一开始就以锁不变量的推理形式包含了并发性，但并发分离逻辑（CSL）从那时起就有了飞跃式的发展。在本文中，我们描述了努力整合的进步，从虹膜，一个国家的最先进的机械化CSL，到VST。Iris的一些特性（幽灵状态和不变量）在VST中从头开始重新实现;其他特性（Iris证明模式）是从Iris开发中导入的;还有一些特性（原子操作的证明规则）是公理化的，希望它们在未来的版本中成为基础。其结果是一个系统，可以证明在C中实现的复杂的并发程序的正确性，细粒度的锁定和非阻塞原子操作，产生不同的可靠性保证取决于所使用的功能。
2022-07-15 cs.PL
A Higher-Order Logic for Concurrent Termination-Preserving Refinement
高阶并发语言的更精确的正确性证明是困难的：它们涉及到在并发的高级源语言和使用低级共享内存原语的实现之间建立一个保持终止的精化。然而，现有的逻辑证明并发加细要么忽略属性，如终止，或只处理一阶状态。在本文中，我们解决这些限制，扩展虹膜，最近的高阶并发分离逻辑，支持终止保留的细化推理。为了证明这些扩展的功能，我们证明了一个高阶，会话类型的语言的有效实现的正确性。据我们所知，这是第一个能够为这种语言提供编译器正确性证明的程序逻辑。我们的扩展和我们的编译器正确性证明的合理性已经在Coq中机械化。
2017-01-20 cs.LO cs.PL
VeriFx: Correct Replicated Data Types for the Masses
本文提出具备自动证明能力的高级语言 VeriFx，支持在函数式集合上实现并自动验证 RDT，且可转译到 Scala 和 JavaScript；通过其 CRDT 与 OT 库验证了 35 个 CRDT 并复现 OT 正确性研究。
2024-12-06 cs.DC cs.PL
The Correctness of Launchbury's Natural Semantics for Lazy Evaluation
John Launchbury在他的开创性论文“A Natural Semantics for Lazy Evaluation”中证明了他关于指称语义的语义正确性。我们对证明进行了机器检查，发现它失败了，并提供了两种方法来修复它：一种是通过显式堆栈修改自然语义，另一种是通过调整堆的指称语义。
2014-05-13 cs.PL
Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs
针对安全编译链证明中回译步骤复杂的挑战，提出一种基于调用-返回树、分多步进行的 nanopass 回译技术，利用幽灵状态和前向模拟简化证明，并在 Rocq 证明器中实现了机械化验证。
2025-07-16 cs.CR cs.PL
Semantics of (Resilient) X10
我们提出了一个正式的小步结构操作语义的一个大片段的X10，统一过去的工作。该片段涵盖多个位置、堆上的可变对象、排序、\code{try/catch}、\code{async}、\code{finish}和\code{at}构造。这个模型准确地捕获了大量并发、多位置X10程序的行为。此外，我们介绍了一个正式的模型的弹性在X10。在执行X10程序期间，位置可能由于多种原因而失败。弹性X10允许程序继续执行，丢失失败位置的数据和大部分控制状态，并修复全局控制状态，以保持关键语义原则，不变发生在原则和失败掩蔽原则。这些原则允许X10程序员编写干净的代码，在出现位置故障的情况下继续工作。在Coq中，给出的语义已经被机械化了。
2013-12-13 cs.PL
Constructive Galois Connections
伽罗瓦连接是在语义学中构造抽象的基本工具，它们的使用是抽象解释理论的核心。然而，使用证明助手的伽罗瓦连接的机械化仍然限于受限的使用模式，阻止了它们在机械化元理论和认证编程中的普遍应用。本文提出了建设性的伽罗瓦连接，伽罗瓦连接的一个变种，是有效的在纸上和证明助手;是完整的一个大子集的经典伽罗瓦连接，并使更一般的推理原则，包括“计算”的风格所倡导的库索。为了设计建设性的伽罗瓦连接，我们确定了一个限制模式的使用经典的，这是通用的，并服从机械化依赖类型的功能程序设计语言。我们的元理论的关键是在伽罗瓦连接中加入一元结构，以控制“规范效应”。“精确的计算可能是经典的，而纯粹的计算具有可提取的计算内容。我们的元理论使我们能够在规范和实现的世界之间进行明确的移动。为了验证我们的方法，我们提供了两个案例研究，在机械化现有的证明文献：第一个使用计算抽象解释设计一个静态分析器;第二个形成了语义基础逐步打字。这两个机械化的证明密切遵循其原来的纸和笔的同行，采用推理原则没有捕捉到以前的机械化方法，支持提取验证算法，是新颖的。
2018-07-23 cs.PL
A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
Nangyang Technological University（南洋理工大学）；Mohamed bin Zayed University of Artificial Intelligence（穆罕默德·本·扎耶德人工智能大学）；East China Normal University（华东师范大学）
本文提出Minilang，一种简洁的证明语言，用于提升神经定理证明在形式证明中的性能。
2025-12-23 cs.PL
Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
我们给出了一个语言参数的解决方案的问题，总的正确性，通过自动减少它的问题的部分正确性，在假设下，提供了一个表达式，其值随着每个程序步骤在一个良好的基础顺序减少。我们的方法假设，程序设计语言的语义是作为一个重写理论。我们实现了一个原型上的RMT工具，我们表明，它在实践中的一些例子。
2019-02-22 cs.LO cs.PL
Logical Relations for Formally Verified Authenticated Data Structures
本文提出基于新型关系分离逻辑的形式化证明方法，为可自动生成认证数据结构的库验证安全性与正确性，证明了库优化的正确性及手写实现与自动生成代码的可靠链接，结果已在Coq中通过Iris框架机械化验证。
2025-01-18 cs.LO cs.PL
MGQL: An Executable, Small-Step Semantics of GQL
University of Texas at Austin（德克萨斯大学奥斯汀分校）
MGQL是首个基于ISO/IEC 39075标准的GQL机械化小步操作语义，解决了现有形式化方法的不足，为GQL规范与机械化实现搭建桥梁，可对查询正确性进行形式化推理。
2026-08-26 cs.DB cs.PL
Denotational Correctness of Forward-Mode Automatic Differentiation for Iteration and Recursion
本文为含部分操作、惰性条件、迭代及项和类型递归的语言，基于微分空间与部分性单子，通过子余构造的语义逻辑关系，给出了前向模式自动微分宏的指称正确性证明，并引入带ωcpo结构的空间扩展至递归情形。
2024-05-27 cs.PL
Towards Correctness of Program Transformations Through Unification and Critical Pair Computation
在具有上下文语义的扩展lambda演算中，程序转换的正确性通常基于对操作语义的推理，该操作语义是重写语义。证明正确性的一个成功的方法是将上下文引理与程序转换和归约规则之间的重叠计算相结合，然后是所谓的完整图集。该方法类似于项重写系统完备化的临界对计算。我们探讨的情况下，这些重叠的计算可以在一阶的方式通过使用统一算法的关键对计算的变体。作为一个案例研究，我们应用该方法的λ演算与递归让表达式，并描述了一个有效的统一算法，以确定所有重叠的一组转换与所有减少规则。统一算法采用了许多排序的条款，左交换建模多集，上下文变量的不同种类和一个机制，competencies表示绑定链递归让表达式的方程理论。
2010-12-22 cs.PL
Deriving Abstract Interpreters from Skeletal Semantics
本文提出一种基于骨架语义及其语义元语言抽象解释的方法，从编程语言形式化语义派生可执行抽象解释器，并通过小型命令式语言的值分析验证了其通用性与正确性。
2023-09-13 cs.PL
Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Extended Version)
本文提出一种基于幽灵的并发程序正确性见证格式，使交错语义与线程模块化语义下的见证有效性一致，并在SV-COMP基准上验证了其可行性。
2024-11-25 cs.PL
Towards the Future: Bring Program Correctness back to the focus
在形式语义是一个热门话题的早期，程序正确性曾经是计算机软件的主要关注点。但是，“正确”一词后来被可靠、稳健和值得信赖等取代，一个折衷的情况。这并不是因为正确性不再重要，而是因为人们发现没有办法在这个方向上取得成功。这种权衡导致软件工程师专注于技术和测试工具。软件工程的快速发展现在已经达到了一个高峰，程序员现在可以自由地工作，而不用太担心bug，因为bug是无法避免的。今天讨论程序正确性有意义吗？我们的答案是肯定的。现在是再次认真考虑正确性的时候了，在为时已晚之前，为未来做好准备。下一代计算机系统在语法（静态）和语义（动态）上都应该是正确的。第一作者的《OESPA：面向语义的编程理论》（2019）一书为语义研究开辟了新的方向。从理论上讲，基于OESPA，可以从程序文本中计算出程序语义，从而证明程序的正确性。但是，当程序规模较大时，语义计算和正确性证明无法手工完成。自动工具是必要的。本文的工作为开发所需的自动化工具奠定了基础，从而丰富了OESPA，使之更好地服务于未来的需要。为此，提出了条件语义谓词的概念。对OESPA中的语义函数、语义谓词、语义公式和语义演算等概念进行了重新表示。这种重新介绍是必要的，因为这本书是唯一的出版物语义演算迄今为止。新版本的语义演算说明了如何进行语义自动计算。
2022-03-29 cs.PL cs.SE
TypeDis: A Type System for Disentanglement
New York University（纽约大学）；Carnegie Mellon University（卡内基梅隆大学）
TypeDis是一种基于时间戳的类型系统，用于自动验证并行程序的解缠属性，通过类型检查确保程序正确性，减少手动证明的工作量。
2025-12-02 cs.PL
Automatic Differentiation for ML-family languages: correctness via logical relations
针对 ML 家族语言，提出一种逻辑关系技术，通过将语言解释为自由生成范畴结构，证明双数风格 AD 代码转换的正确性，可生成正确的前向和反向模式 AD，关键技术为单子逻辑关系。
2024-06-14 cs.PL
LFPL: Revisited and Mechanized
Carnegie Mellon University（卡内基梅隆大学）
本文重新审视并机械化了LFPL语言及其元理论，提供自包含且易懂的现代描述，简化了已知最强的正确性与完备性结果。
2026-07-10 cs.CC cs.LO cs.PL
Industrial Experiences with a Formal DSL Semantics to Check the Correctness of DSL Artifacts
领域特定语言（DSL）从实现细节中抽象出来，并与领域专家对软件组件的推理方式保持一致。DSL的开发通常围绕生成实现代码或分析模型的语法和转换。语言的语义通常是隐式定义的，并根据实现代码的转换来定义。在存在来自DSL的多个转换的情况下，生成的工件相对于DSL的语义的正确性是一个相关的问题。我们表明，一个正式的语义是必不可少的检查生成的工件的正确性。我们利用工业项目中的形式语义，并使用基于等价性检查和基于模型的测试验证生成的工件的正确性的形式化技术。我们报告我们的经验，这种方法在一个工业发展项目。
2016-03-29 cs.LO cs.PL cs.SE
The Denotational Semantics of SSA
该研究提出SSA变体的类型论与范畴语义，证明其可靠完备，给出含TSO弱内存模型的实例，且相关证明已在Lean中机械化，为编译器变换验证提供语义基础。
2024-12-12 cs.LO cs.PL
Proving Correctness and Completeness of Normal Programs - a Declarative Approach
我们提倡使用声明性方法来证明逻辑程序的属性。完全正确性可以分为正确性、完整性和干净终止;后者包括非挣扎。只有干净的终止依赖于操作语义，特别是选择规则。我们展示了如何处理的正确性和完整性的声明方式，治疗程序只从逻辑的角度来看。这种方法中使用的规范是解释（或理论）。我们指出，规范的正确性可能不同于那些完整性，因为通常有答案，既不被认为是错误的，也不需要计算。给出了确定性程序正确性和完备性的证明方法，并将其推广到正规程序。对于正常的程序，我们使用3值完成语义;这是一个标准的语义对应于否定有限失败。证明方法仅采用经典的2值逻辑。我们使用的3值完成语义，这可能是单独的利益的2值表征。所提出的方法进行了比较与基于操作语义的方法。我们还采用这项工作的想法推广一个已知的方法证明终止正常程序。
2005-01-25 cs.LO cs.PL
Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing
我们提出了自动微分（AD）的语义正确性证明。我们考虑一个高阶语言的前向模式AD方法与代数数据类型，我们把它作为一个独特的结构保持宏给出了基本操作的衍生物的选择。我们描述了一个丰富的语义可微编程，基于拓扑空间。我们表明，它解释我们的语言，我们的短语是什么意思的AD方法是正确的，就这个语义。我们表明，我们的AD的特性产生了一个优雅的语义证明其正确性的基础上胶合结构的拓扑空间。我们解释这在本质上是一个逻辑关系论证。最后，我们勾勒出如何分析扩展到其他AD方法，考虑基于连续的方法。
2020-04-01 cs.LO cs.PL
An Inductive Proof Method for Simulation-based Compiler Correctness
我们研究归纳的程序结构作为一种证明方法的基于双模拟的编译正确性。我们考虑一个一阶语言与相互递归的函数定义，系统调用，和一个环境语义。证明方法依赖于函数定义与互模拟的兼容性的推广。我们用归纳法证明了一种死代码消除形式的正确性。这是一个有趣的案例研究，因为转换从程序中删除了函数、变量和参数定义。虽然这样的转换需要修改的模拟在一个共同归纳的证明，归纳法处理他们自然。我们所有的结果都在Coq中形式化了。
2016-11-29 cs.PL
KEM-IND-CCA-Preserving Compilation of Jasmin's ML-KEM
MPI-SP（马克斯·普朗克软件系统研究所）；IMDEA Software Institute（IMDEA软件研究所）；Inria（法国国家信息与自动化研究所）；Université de Lorraine（洛林大学）
该研究在Rocq证明器中机械化证明Jasmin编译器保持Signal所用ML-KEM实现的功能正确性与KEM-IND-CCA安全性，提出三项相关通用贡献。
2026-08-18 cs.CR cs.PL
Proving Correctness of Parallel Implementations of Transition System Specifications
在本文中解决的总体问题是长期存在的问题，程序的正确性，特别是程序，描述系统的并行执行过程。我们提出了一种新的方法来证明高级别的转换系统规范的并行实现的正确性。该方法的实现语言基于活动（或并发）对象模型。该方法根据指定程序语义的转换系统和由正确性规范描述的转换系统之间的模拟关系来定义正确性。模拟关系本身抽象的细粒度交错的并行进程，利用本文所考虑的活动对象的特定模型的全局汇合属性。作为一个概念验证，我们将我们的方法的正确性的多核内存系统的并行模拟器。
2023-01-25 cs.PL
Verified VCG and Verified Compiler for Dafny
ETH Zurich Switzerland；Chalmers University of Technology\ of Gothenburg Sweden；Institute for Infocomm Research (I 2 R), A STAR Singapore；Nanyang Technological University Singapore；ETH Zurich；Chalmers University of Technology\ of Gothenburg；Institute for Infocomm Research (I 2 R), A STAR；Nanyang Technological University
本文提出通过形式化方法验证Dafny语言的VCG和编译器，确保程序的正确性并生成可执行代码。
2025-12-04 cs.LO cs.PL
Foundational Refinement Proofs for EVM Bytecode, at the Price of Tokens
Argot Collective；National Technical University of Athens（雅典国立技术大学）
该研究构建了Lean框架EquiVM，利用前沿LLM以代币为代价，为EVM上23个真实合约生成了可复现的基础精化机器证明，实现了此前技术未达的特性组合，重塑验证框架架构。
2026-10-21 cs.PL
Certifying C program correctness with respect to CompCert with VeriFast
VeriFast是一个强大的工具，用于验证使用符号执行的C程序的各种正确性属性。然而，VeriFast本身尚未得到验证。我们提出了一个概念验证扩展，为每个成功的验证单独运行生成一个正确性证书。此证书采用Coq脚本的形式，其中包含两个证明，当Coq成功检查时，就不再需要信任VeriFast本身的正确性。第一个证明了一个引理，该引理表达了程序相对于我们开发的一个大步操作语义的正确性，旨在反映VeriFast对C语言的解释。我们在Coq中将这种语义形式化为cbsem。这个引理通过Coq中的符号执行来证明，而Coq又通过将程序的导出AST转换为表示VeriFast本身执行的符号执行的Coq命题来实现。第二个证明了同一个C程序在CompCert的Clight大步语义方面的正确性。这个证明简单地将我们对cbsem关于CompCert Clight的可靠性的证明应用于第一个证明。
2021-10-21 cs.LO cs.PL
A Simple Correctness Proof for Magic Transformation
本文给出了幻变换正确性的一个简明证明。我们相信它可以提供一个有用的例子形式推理的逻辑程序。正确性属性涉及声明性语义。然而，证明涉及源程序的操作语义（LD解析）。它的简洁性是由于应用了适当的证明方法。
2010-12-10 cs.DB cs.LO cs.PL
On correctness of an n queens program
Thom Frühlynth提出了一个简短，优雅和有效的Prolog程序的n皇后问题。然而，该程序可能被视为相当棘手，人们可能不相信它的正确性。本文以声明的方式解释了程序，并证明了程序的正确性和完整性。规范和证明是声明性的，即它们从任何操作语义中抽象出来。该规范是近似的，不需要精确地描述程序的语义。尽管该程序的工作在非地面条款，这项工作采用了标准的语义，基于逻辑后果和Herbrand解释。本文的另一个目的是提出一个关于逻辑程序语义的精确声明推理的例子。
2020-07-17 cs.LO cs.PL cs.SE
Corten - Foundational Verification of Rust Programs
Barkhausen Institute（巴特豪森研究所）；Kernkonzept GmbH（Kernkonzept有限公司）
Corten是基于Iris分离逻辑的Rust程序基础验证框架，在Rocq中实现了Rust表层语义，可缩小证明规模并验证伙伴分配器的内存安全，为跨软硬件的端到端验证奠基。
2026-09-07 cs.PL
Industrial Experiences with a Formal DSL Semantics to Check Correctness of DSL Transformations
领域特定语言（DSL）从实现细节中抽象出来，并与领域专家对软件组件的推理方式保持一致。DSL的开发通常围绕生成实现代码或分析模型的语法和转换。语言的语义通常是隐式定义的，并根据实现代码的转换来定义。在存在来自DSL的多个转换的情况下，生成的工件相对于DSL的语义的一致性是一个相关的问题。我们表明，一个正式的语义是必不可少的检查生成的工件之间的一致性。我们利用工业项目中的形式化语义，并使用形式化技术的基础上，等价性检查和基于模型的测试的一致性检查。我们报告我们的经验，这种方法在一个工业发展项目。
2015-11-25 cs.LO cs.PL cs.SE
A Lambda-Calculus Foundation for Universal Probabilistic Programming
我们开发的操作语义的无类型的连续分布的概率λ演算，通用概率程序设计语言，如教会，圣公会，和风险的基础。我们的第一个贡献是适应经典的操作语义的连续设置，通过创建一个测量空间的条款和定义步骤索引的近似。我们证明了这种基于分布的语义的大步和小步配方的等价性。为了更接近推理技术，我们还将术语的基于采样的语义定义为从随机样本的轨迹到值的函数。我们表明，通过整合所有的痕迹，导致的分布等于基于分布的语义。我们的第二个贡献是形式化的跟踪马尔可夫链蒙特卡罗（MCMC）的实现技术，我们的演算，并显示其正确性。一个关键的步骤是定义充分条件的分布引起的跟踪MCMC收敛到基于分布的语义。据我们所知，这是高阶函数式语言的跟踪MCMC的第一个严格正确性证明。
2017-01-23 cs.PL
AutoVeriFix+: High-Correctness RTL Generation via Trace-Aware Causal Fix and Semantic Redundancy Pruning
Microelectronics Thrust, the Hong Kong University of Science and Technology (Guangzhou)（微电子交叉学科，香港科技大学（广州））
AutoVeriFix+通过轨迹感知因果修复和语义冗余剪枝，提升Verilog代码生成的功能正确性与设计效率。
2026-03-12 cs.AR cs.PL
When Do Staging Annotations Preserve Semantics? Mechanizing Typed Semantics-Preserving Multi-stage Programming with Let-Insertion (Extended Version)
Tufts University（塔夫茨大学）
研究带引用的多阶段编程中阶段注释保持语义的条件，提出两个带类型的两阶段演算，通过自动let插入和轻量类型-效应系统实现语义保持，并证明强语义保持定理。
2026-08-24 cs.PL
On correctness and completeness of an n queens program
Thom Frühlynth提出了一个简短，优雅和有效的Prolog程序的n皇后问题。然而，该程序可能会被视为相当棘手，人们可能不会相信它的正确性。本文以声明的方式解释了程序，并证明了程序的正确性和完整性。规范和证明是声明性的，即它们从任何操作语义中抽象出来。该规范是近似的，不需要精确地描述程序的语义。尽管该程序的工作在非地面条款，这项工作采用了标准的语义，基于逻辑后果和Herbrand解释。本文的另一个目的是提出一个关于逻辑程序语义的精确声明推理的例子。逻辑程序设计理论与实践（TPLP）
2021-08-18 cs.LO cs.PL cs.SE
Spreadsheet Guardian: An Approach to Protecting Semantic Correctness throughout the Evolution of Spreadsheets
电子表格是一种强大的工具，在许多组织中发挥着关键的业务作用。然而，由于错误的电子表格而做出的许多错误决定表明，这些工具需要认真的质量保证。此外，虽然在维护任务的电子表格上进行协作是常见的，但几乎没有任何支持来确保电子表格在此过程中保持正确。我们已经开发出一种名为电子表格监护人的方法，它分离的规范电子表格测试规则，从他们的执行。通过自动执行用户定义的测试规则，我们的方法是能够检测语义故障。它还保护所有协作的电子表格用户在维护期间避免引入错误，即使只有少数最终用户指定测试规则。为了评估Spreadsheet Guardian，我们实施了一种代表性的测试技术作为Microsoft Excel的加载项。我们评估了测试技术在两个实证评估与29最终用户和42计算机科学的学生。结果表明，该技术简单易学，易于应用。此外，完成维护后，与电子表格“保护”的技术的参与者更现实的正确性，他们的电子表格比参与者谁只采用“经典”，非交互式的测试规则的基础上静态分析技术。因此，我们相信电子表格守护者可以用于业务关键型电子表格。
2017-11-30 cs.PL cs.SE
A Semantics for Approximate Program Transformations
近似程序转换是一种可以在指定的经验误差范围内改变程序语义的转换。这种转换有广泛的应用：它们可以减少计算时间，功耗和内存使用，并且在某些情况下，可以允许实现不可计算的操作。近似程序变换的正确性证明是定量的。不幸的是，与标准程序转换不同，目前还没有模块化的方法来证明近似转换本身的正确性。误差界必须证明每个转换程序单独，并必须重新证明每次修改程序或一组不同的近似应用。在本文中，我们给出了一个语义，使定量推理的一个大类的近似程序变换的本地，组合的方式。我们的语义是基于程序之间的距离的概念，它定义了一个近似变换是正确的错误界意味着什么。关键的见解是，程序之间的距离一般不能用度量空间和实数来表示。相反，我们的语义承认每个类型构造的距离的自然概念;例如，数字被用作数值数据的距离，函数被用作函数数据的距离，多态数据项被用作多态数据的距离。然后，我们将展示我们的语义如何应用于两个示例近似：用浮点数替换实数和循环穿孔。
2013-04-19 cs.PL
Beyond BLEU: A Semantic Evaluation Method for Code Translation
TU Darmstadt（图宾根大学）；Hessian Center for Artificial Intelligence（黑森人工智能中心）；National Research Center for Applied Cybersecurity ATHENE（应用网络安全国家研究中心ATHENE）
本文提出一种基于语义等价的代码翻译评估方法，通过编译器测试方法评估LLM的二进制提升任务性能，发现语义正确性得分与BLEU得分无显著相关性。
2026-05-06 cs.CL cs.PL
jMT: Testing Correctness of Java Memory Models (Extended Version)
Carl von Ossietzky Universität Oldenburg（奥尔登堡卡尔·冯·奥西茨基大学）
jMT通过构建多执行语义来验证Java内存模型的正确性，支持对新提案的JMM进行程序级别的评估，并测试其与现有编译方案的兼容性。
2026-04-17 cs.PL
Correctness Kernels of Abstract Interpretations
在基于抽象解释的静态分析中，近似是由抽象域编码的。它们为设计抽象语义函数提供了系统的指导，这些抽象语义函数近似于分析中的某些具体系统行为。为了近似给定的具体语义功能，抽象域可能包含冗余信息。本文介绍了抽象解释的正确性核的概念，一种简化抽象域的方法，即从它们中删除抽象值，以最大的方式，同时保留完全相同的近似行为的系统分析。我们表明，在抽象的模型检验正确性内核提供了一个由示例指导的抽象状态空间的简化范例，这意味着这种简化保留了示例的虚假性（即，抽象路径）。特别是，我们展示了如何正确的内核可以集成与著名的CEGAR（反例引导的抽象细化）方法。
2013-04-19 cs.LO cs.PL
Symbolic Semantics for Probabilistic Programs (extended version)
本研究基于Kozen的工作提出含observe语句与连续分布采样的概率程序的新型符号执行语义，完成正确性证明，在symProb工具中实现并通过示例验证。
2023-07-19 cs.PL
Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
本文针对地理复制系统中的弱一致性并发库，提出语义与规范，并开发静态分析框架以自动检测正确性违规，首次证明此类自动检查可行且实用。
2020-04-21 cs.PL
A Term-Rewriting Semantics for Imperative Style Programming
术语重写系统具有简单的语法和语义，并且便于正确性证明。然而，它们在工业界或学术界并不像命令式语言那样受欢迎。我们定义了一个术语重写为基础的抽象程序设计语言与一个命令式的风格和精确的语义，允许程序翻译成高效的命令式语言，以获得证明的正确性与高效的执行。这种语言的目的是促进翻译成正确的程序在命令式语言的赋值语句，迭代，递归，数组，指针和副作用。它也可以用来代替伪程序设计语言来指定算法。
2020-07-06 cs.PL cs.SE
Certifying C program correctness with respect to CH2O with VeriFast
本文提出一个概念验证扩展，为 VeriFast 的每次成功验证生成 Coq 证书，通过可靠性证明链将程序正确性归约到 CH2O 语义，从而消除对 VeriFast 本身的信任需求。
2023-08-29 cs.LO cs.PL
All-Path Reachability Logic
本文提出全路径可达性逻辑，一种语言无关的证明系统，用于验证非确定性程序的可达性属性，具有可靠性和相对完备性，并在 Coq 中机械化验证，已实现于 K 框架。
2019-04-29 cs.FL cs.LO cs.PL
Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics
Zhejiang University（浙江大学）；Runtime Verification Inc.（运行时验证公司）
提出“通过证明进行编译”范式，利用验证证明构造全路径可达性证明并编译其图结构，实现语言无关的自动优化，实验显示操作码级一致加速及全程序数量级性能提升。
2025-09-26 cs.CL cs.PL
Correctness-Guaranteed Code Generation via Constrained Decoding
Netflix
本文提出一种基于上下文敏感解析器和动态解析器树的约束解码算法，通过sLua生成符合指定API的语义正确代码，并将保证扩展到运行时正确性，在roguelike游戏机制生成中得到验证。
2025-08-20 cs.LG cs.PL cs.SE
Logical Relations for Partial Features and Automatic Differentiation Correctness
我们提出了一个简单的技术，语义，开放的逻辑关系参数与递归类型的语言，其中，正如我们所示，遵循从分类语义的原则基础。我们演示了它如何可以用来给一个非常简单的证明的正确性的实际正向和反向模式的双数风格自动微分（AD）ML-家庭的语言。的关键思想是将其与一个合适的开放的逻辑关系的推理技术可微的部分功能（一个合适的提升的单根逻辑关系），我们介绍。
2022-10-24 cs.LO cs.PL math.CT
Automating the Diagram Method to Prove Correctness of Program Transformations
我们报告的自动化技术，以证明程序转换的正确性，在高阶程序演算，这可能允许递归让绑定，因为它们发生在功能程序设计语言。如果程序转换保持了程序的观察语义，那么它就是正确的。在我们的LRSX工具中，所谓的图方法是通过结合高阶元语言上的α重命名的统一、匹配和推理来自动化的，并且通过编码来自动化归纳证明到术语重写系统的终止问题中。我们解释的技术，我们说明了使用的工具，我们报告的实验。
2019-02-22 cs.LO cs.PL
