Reasoning about Recursive Quantum Programs
大多数现代（经典）程序设计语言都支持递归。递归也被成功地应用于几种量子算法的设计，并被引入到几种量子程序设计语言中。因此，可以预期递归将成为量子编程的基本范式之一。已经开发了几种程序逻辑来验证量子while程序。然而，在量子计算（测量）中，还没有通用的方法来推理（互）递归过程和辅助量子数据结构。我们提出了一种参数化的量子断言逻辑，并在此基础上设计了一种量子霍尔逻辑，用于验证带有辅助数据和概率控制的参数化递归量子程序.量子霍尔逻辑可以用来证明这些量子程序的部分正确性、全部正确性，甚至概率正确性（通过简化为全部正确性）。特别是，两个反例说明不完整的非参数化断言在验证递归过程中，和，一个反例显示失败的推理与精确概率的基础上部分正确性，构造。我们的逻辑的有效性是由三个主要的例子-递归量子马尔可夫链（概率控制），不动点格罗弗的搜索，和递归量子傅立叶采样。
2021-07-24 cs.LO cs.PL
Building Extensible Program Logics through Effect Handlers
New York University（纽约大学）；CISPA Helmholtz Center for Information Security（CISPA赫尔姆霍兹信息安全中心）
本文提出基于效应处理程序构建可扩展程序逻辑的方法，从表达性程序逻辑出发，实现模拟多种行为的处理程序并证明其属性以扩展逻辑，还开发关系逻辑，该方法能产生更强推理规则且可扩展。
2026-07-15 cs.LO cs.PL
Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs
我们提出了定量分离逻辑（$\mathsf{QSL}$）。与经典的分离逻辑相反，$\mathsf{QSL}$采用计算为实数的量，而不是计算为布尔值的谓词。将经典分离逻辑的连接词分离合取和分离蕴涵从谓词提升为量。这个扩展是保守的：这两个连接词是向后兼容的经典类似物，并遵守相同的法律，例如肯定前件，伴随性等。此外，我们开发了一个最弱的前提演算概率指针程序的定量推理$\mathsf{QSL}$。这种演算是Reynolds的堆操作程序的分离逻辑和Kozen/ McIver和Morgan的概率程序的最弱预期望的保守扩展。可靠性证明相对于一个基于马尔可夫决策过程的操作语义。我们的演算保留了O 'Hearn的框架规则，使本地推理。我们证明，我们的演算能够推理数量，如终止与空堆的概率，达到一定的数组排列的概率，或列表的预期长度。
2018-11-26 cs.LO cs.PL
Reasoning about Choreographic Programs
本文针对编排编程领域其他性质验证研究不足的问题，提出一种Hoare风格的编排行为推理逻辑，证明其可靠性与完备性，且编排的功能正确性性质可传递至编译后的分布式实现。
2023-04-27 cs.LO cs.PL
A Concurrent Program Logic with a Future and History
细粒度的乐观并发程序仍然是一个悬而未决的问题。现代程序逻辑提供了抽象机制和组合推理原则来处理固有的复杂性。然而，它们的使用主要局限于纸张和纸张或机械化的证明。我们设计了一个新的分离逻辑，面向缺乏自动化。虽然本地推理是众所周知的自动化是至关重要的，我们是第一个展示如何保持这种局部性（i）推理归纳属性，而不需要幽灵代码，和（ii）推理计算历史的事后诸葛亮。我们在一个工具中实现了我们的新逻辑，并使用它来自动验证具有挑战性的并发搜索结构，这些结构需要归纳属性和事后推理，例如Harris集。
2022-11-11 cs.LO cs.PL
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
提出Coneris，首个高阶并发分离逻辑，通过随机逻辑原子性支持并发概率程序的错误概率界模块化推理，并在Rocq和Iris中机械化验证。
2025-08-07 cs.LO cs.PL
The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
我们提出了守护的Alguda演算，简单类型的Alguda演算与守护递归和共归纳类型的扩展。保护递归类型的使用确保了良好类型程序的生产力。受模态逻辑和Atkey-McBride时钟量化启发的类型生成器可以将受保护的递归类型转换为共归纳类型，从而允许非因果函数的类型化。我们给出了演算的按名调用操作语义，并在树的拓扑中定义了适当的指称语义。充分性证明意味着程序的评估总是终止的。我们介绍了一个程序逻辑与Löb归纳推理的上下文等价的程序。我们展示了表现力的演算显示的可定义性的解决方案Rutten的行为微分方程。
2016-09-05 cs.LO cs.PL
Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
本文提出结果分离逻辑（OSL），一种同时支持正确性与不正确性推理的程序逻辑，通过框架规则和新的三归结符号执行算法，实现对具有计算效应程序的局部推理，推进了分离逻辑的合成性。
2024-03-13 cs.LO cs.PL
Integrating Reasoning Systems for Trustworthy AI, Proceedings of the 4th Workshop on Logic and Practice of Programming (LPOP)
第4届编程逻辑与实践研讨会聚焦于可信人工智能的推理系统集成，将与第40届国际逻辑编程会议联合于2024年10月13日在美国达拉斯以混合形式举行，重点是集成不同编程模型与规则和约束。
2026-07-27 cs.AI cs.LO cs.PL
Bialgebraic Reasoning on Higher-Order Program Equivalence
针对高阶程序上下文等价性推理需逐场景构建逻辑关系的问题，本文在高阶数学操作语义框架下提出步索引逻辑关系的通用构造，证明弱操作模型为松弛双代数时逻辑关系自动可靠，且可实例化到多种演算与等价性场景。
2024-05-16 cs.LO cs.PL
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
我们提出了TaDA现场，一个并发分离逻辑的推理组合终止阻塞细粒度并发程序。关键的挑战是如何处理抽象的原子阻塞：也就是说，抽象的原子操作具有阻塞行为，这些阻塞行为来自于例如细粒度自旋锁中的忙等待模式。我们的基本创新是抽象规范的设计，捕捉这种阻塞行为作为对环境的活跃假设。我们设计了一个逻辑，可以原因的客户端使用这些操作的终止，而不会打破他们的抽象边界，和操作的实现相对于他们的抽象规范的正确性。我们引入了一个新的语义模型，使用分层的主观义务来表达活性不变量，和一个证明系统，这是健全的模型。我们的规范和推理的微妙之处说明了使用几个案例研究。
2021-11-30 cs.LO cs.PL
Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday
这本书是一本散文集，从个人回忆到技术贡献。这是对戴夫·施密特和他的职业生涯的致敬，并在他六十岁生日之际创作。
2013-09-18 cs.LO cs.PL cs.SE
Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version)
近年来，随着操作语义和相关逻辑的发展，C11程序的演绎验证技术有了很大的进步。然而，这些语义和逻辑是在受限的环境中开发的，以避免稀薄空气读取问题。在本文中，我们提出了一个操作语义，利用线程内的偏序（称为语义依赖）诱导最近开发的指称事件结构为基础的语义。我们证明了我们的操作语义是健全的和完整的指称语义。我们提出了一个相关的逻辑，概括了最近Owicki-Gries框架RC 11（修复C11），并证明了使用这种逻辑的几个例子证明。
2021-08-03 cs.LO cs.PL
Reasoning About Exceptional Behavior At the Level of Java Bytecode
本文扩展 ByteBack，提出通过 Vimp 中间层在 Java 字节码层面建模并验证异常行为，可支持多版本 Java 及 Scala、Kotlin。
2024-09-30 cs.LO cs.PL
Complete Local Reasoning About Parameterized Programs Over Topologies (Extended Version)
University of Toronto（多伦多大学）
本文研究了无限状态参数化并发程序在丰富通信拓扑上的算法安全验证问题，提出通过全局量化归纳不变量自动证明正确性的方法，并通过多个拓扑的基准测试验证了该方法的有效性。
2026-07-22 cs.LO cs.PL
Towards a General Framework for Formal Reasoning about Java Bytecode Transformation
程序转换引起了广泛的兴趣，因为它用于多种目的：改变程序的语义、向程序添加功能或执行优化。在本文中，我们专注于程序转换在字节码级别。由于这些转换可能会引入错误，因此我们的目标是提供一种正式的方法来验证更新并确定其正确性。提出的形式化框架定义了更新的形式语义，作为静态验证的基础，并提出了一种基于Hoare三元组和最弱前提演算的字节码转换行为推理方案
2013-07-31 cs.LO cs.PL
Elton: Urn Resources for Reasoning about Adversarial Probabilistic Programs
Aarhus University（奥胡斯大学）；New York University（纽约大学）
研究对抗性概率程序，提出埃尔顿这一高阶分离逻辑，利用语言层面延迟采样和逻辑层面瓮资源等工具，结合其他特性，能证明安全示例错误界限，且证明已机械化验证。
2026-07-16 cs.LO cs.PL
Certifying and reasoning about cost annotations of functional programs
我们提出了一个所谓的标签的方法插入成本注释在高阶函数程序，以证明他们的正确性相对于一个标准的编译链，汇编代码，包括安全的存储管理，并对他们的原因在高阶霍尔逻辑。
2013-01-16 cs.PL
Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs
我们提出了一种程序推理的方法，它在程序及其验证条件之间插入一个附加层，即以声明形式表示的程序的外延。首先将程序翻译成其表示，随后从该表示生成验证条件。然而，即使在任何验证尝试之前（并且独立于任何验证尝试），人们也可以调查指称本身以洞察程序的“语义本质”，特别是看看指称是否确实给出了相信程序具有预期行为的理由。因此，在实际执行形式化验证之前，可以检测并修复程序和元信息中的错误。更具体地说，程序语义的关系方法，我们建模的程序作为一个二元关系的程序状态的影响。一个正式的演算是从一个程序中推导出一个逻辑公式，描述这种关系，并进行检查和操作。我们已经实现了这一想法在RISC ProgramExplorer，一个新的程序推理环境的教育目的，其中包括以前开发的RISC ProofNavigator作为一个交互式的证明助理的全面形式。
2012-02-22 cs.LO cs.MS cs.PL
Lifting the Reasoning Level in Generic Weak Memory Verification (Extended Version)
本文提出基于视图断言语言的抽象证明规则，将通用弱内存验证的推理从低层公理提升至程序构造层次，并在WRC测试上验证，显著减少证明步骤。
2023-09-04 cs.LO cs.PL
Toward a Theory of Programming Language and Reasoning Assistant Design: Minimizing Cognitive Load
当前使程序设计语言和推理助手对人们更有效的方法集中于利用来自用户的反馈和评估特定技术的成功。这些方法虽然有帮助，但可能不会产生尽可能可用的系统，并且可能不会导致一般的设计原则。本文主张利用认知科学的理论，重点是认知负荷理论，设计更有效的程序设计语言和推理助手。这些理论的发展可以使设计者以更低的成本创造更有效的程序设计语言和推理助手。
2021-10-24 cs.PL cs.SE
Reasoning about Iteration and Recursion Uniformly based on Big-step Semantics
可靠的演绎程序验证技术应该被证明是相对于程序设计语言的语义合理的。对于每一种不同的语言，构造一个单独的可靠性证明往往是一项艰巨的任务。在独立于语言的程序验证中，讨论了计算机程序的共同方面，以使所有语言都能进行合理的推理。在这项工作中，我们提出了一个解决方案，合理的推理迭代和递归的基础上的大步骤操作语义的任何程序设计语言。我们给出了我们的推理技术的合理性和相对完整性的归纳证明。我们说明了在简化的程序设计语言的命令式和功能的范例，具有不同的功能的技术。我们还在Coq证明助手中机制化所有正式结果。
2021-08-04 cs.PL
Reasoning about Parallel Quantum Programs
通过定义并行量子程序的操作语义和指称语义，我们开始了对并行量子程序的研究。本文的技术贡献包括：（1）为并行量子程序的正确性推理找到了一系列有用的证明规则;（2）证明了一个不相交并行量子程序部分正确性证明规则的（相对）完备性;以及（3）证明证明规则的强可靠性定理，表明部分正确性在操作中的每一步转换都得到了很好的维护。通用并行量子程序的语义（具有共享变量）。这是通过部分克服经典并行编程中从未存在的以下概念挑战来实现的：（i）由量子测量引起的非确定性的交织和并行性的引入;（ii）组件量子程序之间的纠缠;以及（iii）在组件量子程序的状态希尔伯特空间与共享变量的重叠中组合量子谓词。本文中开发的技术的应用说明了一个形式化验证的Bravyi-Gosset-König的并行量子算法解决线性代数问题，这给了第一次的计算量子优势的无条件证明。
2019-10-01 cs.LO cs.PL quant-ph
Relational program synthesis with numerical reasoning
University of Oxford（牛津大学）
程序合成方法努力学习具有数值的程序。一个特别困难的问题是在多个示例中学习连续值，例如区间。为了克服这个限制，我们引入了一个归纳逻辑程序设计方法，它结合了关系学习与数值推理。我们的方法，我们称之为NUMSYNTH，使用可满足性模理论求解器，有效地学习程序的数值。我们的方法可以识别线性算术片段中的数值，如实数差分逻辑，以及无穷域中的数值，如实数或整数。我们在四个不同领域的实验，包括游戏和程序合成，表明我们的方法可以（i）学习程序的数值线性算术推理，（ii）优于现有的方法在预测精度和学习时间。
2022-10-04 cs.LG cs.PL
Reasoning About a Service-oriented Programming Paradigm
本文介绍了一种新的分布式应用程序开发方法：面向服务的方法。这是一个概念文件的基础上，我们的经验，在开发一个理论和编程服务的语言。理论形式化和语言解释器都向我们展示了一种新的编程范式存在的证据。在本文中，我们说明了它的基本特征。
2009-06-22 cs.DC cs.PL
$ω$PAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs
本文提出 ωPAP 空间范畴作为指称语义框架，以统一处理高阶递归概率与可微程序，并据此证明自动微分正确性及概率程序迹密度的几乎处处可微性。
2023-05-25 cs.LG cs.LO cs.PL
When is LLM-Based Program Reasoning Correct? A Completion Semantics for LLM-Based Code Inference
Nanjing University（南京大学）；National University of Singapore（新加坡国立大学）
研究基于大语言模型的程序推理何时正确，引入补全语义，将不完整程序形式化，定义存在性推理正确性。以见证生成工作流程实例化方法，在真实任务上评估，能区分合理与不合理推理，为验证不完整程序推理提供实用机制。
2026-09-15 cs.PL
Example-Based Reasoning about the Realizability of Polymorphic Programs
本文研究参数性、输入输出示例与草图之间的交互，提出利用容器态射表示多态函数，并通过转换到容器设定实现多态程序可实现性的自动推理，以辅助程序合成中的搜索空间剪枝。
2024-07-08 cs.PL
An approach to translating Haskell programs to Agda and reasoning about them
我们使用Agda程序设计语言和证明助手来正式验证基于HotStuff / LibraBFT的拜占庭容错共识实现的正确性。Agda实现是我们基于LibraBFT的Haskell实现的翻译。这篇简短的论文集中在这项工作的一个方面。我们开发了一个库，使翻译后的Agda实现能够紧密地反映它所基于的Haskell代码。这使得更容易和更有效地审查翻译的准确性，并在Haskell代码更改时维护翻译的Agda代码，从而降低翻译错误的风险。我们还解释了我们如何捕捉我们的库提供的语法功能的语义，从而使正式的推理程序使用它们，我们如何推理所产生的Agda实现的细节将在未来的论文。我们提供的库独立于我们的特定验证项目，并且是开源的，可供其他人使用和扩展。
2022-05-18 cs.LO cs.PL cs.SE
Quantitative Strongest Post
我们提出了一种新的最强后置条件式演算的定量推理的非确定性程序的循环。现有的定量最弱前允许推理程序在给定的初始状态终止后的量的值，定量最强后允许推理程序执行并达到给定的最终状态之前的量的值。我们展示了如何最强的职位，使推理的定量信息流通过程序。与最弱的自由主义前提条件类似，我们也发展了一个数量上最强的自由主义职位。作为一个副产品，我们获得了完全未经探索的最强自由后置条件的概念，并显示这些预示着一个潜在的新的程序逻辑-部分不正确逻辑-这将是一个更自由的版本奥赫恩最近的不正确逻辑。
2022-02-14 cs.CR cs.LO cs.PL
Automatic Reasoning on Recursive Data-Structures with Sharing
我们考虑的问题，自动验证程序操纵任意数据结构。我们的规约语言是表达，包含一个概念的\emph{separation}，从而使一个精确的规范\emph{frames}。然后，主要贡献是一个程序验证方法，它结合了最强的后置条件推理的形式符号执行，展开递归定义的数据结构的问题，和一个新的框架规则，以实现\emph{local reasoning}，使证明可以组合。最后，我们提出了一个实现我们的验证，并证明自动化的一些代表性的程序。特别是，我们提出了一个经典的图形标记算法的第一个自动证明，铺平了道路，处理一类程序，遍历一个复杂的数据结构。
2017-11-15 cs.PL
MultiVerse: Causal Reasoning using Importance Sampling in Probabilistic Programming
Babylon Health（巴比伦健康）；University of Oxford（牛津大学）；University College London（伦敦大学学院）
我们详细说明使用重要性采样的因果推理，特别是反事实推理。我们展示了如何在概率编程中本地实现这一点。通过考虑反事实查询的结构，可以显著优化推理过程。我们还考虑设计选择，以实现进一步优化。我们介绍了MultiVerse，一个概率编程的原型引擎近似因果推理。我们提供了实验结果，并与Pyro，现有的概率编程框架与一些因果推理工具进行比较。
2020-01-28 cs.AI cs.LG cs.PL
Diffy: Inductive Reasoning of Array Programs using Difference Invariants
我们提出了一种新的验证技术来证明有趣的性质的一类数组程序的符号参数N表示数组的大小。该技术依赖于构造同一程序的两个稍微不同的版本。推导了两个程序版本的联合控制流图关键控制点上相应变量之间的差异关系。然后通过引入程序参数$N$来证明所需的后置条件，其中差分不变量在归纳步骤中至关重要。这与依赖于为程序中的每个循环找到潜在的复杂循环不变量的经典技术形成对比。我们的归纳推理和寻找简单差异不变量的协同组合有助于证明程序的属性，即使是SV-COMP 2021的数组子类别的获胜者也无法证明这些属性。我们已经实现了一个名为diffy的原型工具来演示这些想法。我们目前的结果比较diffy的性能与国家的最先进的工具。
2021-07-02 cs.PL cs.SE
Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs (Extended Version)
我们研究量子程序的预期运行时间。最近的工作的启发概率程序，我们首先定义预期运行时间作为量子最弱的前提条件的概括。然后，我们证明了量子程序的预期运行时间可以表示为（物理学中的）可观测值的期望。提出了一种在有限维状态空间中计算量子程序期望运行时间的方法。作为该方法的应用提供了几个例子，包括计算量子伯努利工厂的预期运行时间-一种用于生成随机数的量子算法。特别是，使用我们的新方法，解决了由Ambainis等人（STOC 2001）引入的计算量子随机游动的期望运行时间的一个公开问题。
2022-07-14 cs.PL quant-ph
Program Synthesis using Inductive Logic Programming for the Abstraction and Reasoning Corpus
INESCTEC-FCUP
针对 ARC 对强泛化与推理的挑战，本文提出以手工对象中心 DSL 作为背景知识、用 ILP 从少量网格示例合成逻辑程序的系统，并验证其可解决多种不同推理任务。
2024-05-10 cs.AI cs.LG cs.PL
Algebraic Reasoning of Quantum Programs via Non-idempotent Kleene Algebra
受基于Kleene代数的经典程序分析成功的启发，我们研究了量子程序的代数推理。一个突出的例子是著名的Kleene代数与测试（KAT），它提供了理论见解和实用工具。代数推理的简洁性对于量子程序的可扩展分析来说是特别可取的，因为在大多数现有方法中涉及指数大小的矩阵。然而，KAT的一些关键特征，包括幂等律和经典测试的良好性质，由于其独特的量子特征，特别是在分支中，在量子程序的背景下无法保持。我们提出了非幂等Kleene代数（NKA）作为一个自然的选择，并确定完整和健全的语义模型NKA以及它们的量子解释。结合KAT的应用，给出了量子编译优化的NKA代数证明和量子while程序的范式。此外，我们用测试扩展NKA（即，NKAT），其中测试模型量子谓词以下的效果代数，并说明如何编码命题量子霍尔逻辑作为NKAT定理。
2022-03-29 cs.PL quant-ph
A Prolog-based Environment for Reasoning about Programming Languages (Extended abstract)
ECLAIR是一个基于Prolog的原型系统，旨在为程序设计语言分析和实现工具的研究、开发和评估提供一个功能完整的环境。在本文中，我们勾画了系统的总体结构，概述了其组件的主要方法和技术。我们还讨论了Prolog作为系统实现语言的适当性：除了突出其优点外，我们还指出了一些潜在的弱点，暗示了可能的解决方案。
2007-11-02 cs.PL cs.SE
Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
针对经典-量子程序因量子测量和无界循环导致的概率行为验证难题，提出含分布公式的量子霍尔逻辑，证明其指称语义可靠性，验证HHL和Shor算法正确性并嵌入Coq形成CoqQLR框架，支持半自动化推理。
2025-02-14 cs.PL quant-ph
The Path Not Taken: Duality in Reasoning about Program Execution
Department of Computer Science, University of Central Florida（中央佛罗里达大学计算机科学系）
本文提出通过双重推理任务评估程序执行的因果理解，提出DexBench基准测试集，评估13种LLM，证明双路径推理能有效提升动态代码理解能力。
2026-04-22 cs.AI cs.CL cs.LG
Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
量子程序设计语言使开发人员能够实现量子计算机的算法，这些算法有望在经典棘手的任务中实现计算突破。对量子计算机进行编程需要意识到纠缠，即量子比特的测量结果相互关联的现象。纠缠可以决定算法的正确性和编程模式的适用性。在这项工作中，我们将纯度形式化为自动推理量子程序中纠缠的核心工具。纯表达式是其评估不受其不拥有的量子比特的测量结果影响的表达式，这意味着在计算中不与任何其他表达式纠缠。我们提出扭曲，第一种语言，具有一个类型系统的健全的推理纯度。类型系统使开发人员能够使用类型注释来标识纯表达式。Twist还具有纯度断言算子，该算子声明量子门的输出中不存在纠缠。为了正确地检查这些断言，Twist使用了静态分析和运行时验证的组合。我们评估了Twist的类型系统，并在模拟中对一套基准量子程序进行了分析，证明了Twist可以表达量子算法，捕获其中的编程错误，并支持几种语言不允许的程序，同时产生的运行时验证开销小于3.5%。
2022-05-04 cs.PL quant-ph
Programming and Reasoning with Partial Observability
计算机程序越来越多地部署在部分可观察的环境中。部分可观测环境是一种其状态对程序不完全可见的环境，但程序从其中接收部分观测。开发人员通常通过编写状态估计器来处理部分可观测性，该状态估计器在给定观测值的情况下尝试推断环境的隐藏状态。在安全关键域中，为了正式验证安全属性，开发人员可以编写环境模型。该模型捕捉观测值和隐藏状态之间的关系，并用于证明软件的正确性。在本文中，我们提出了一种新的方法，在部分可观察的环境中编写和验证程序。我们提出的信念编程，编程方法，开发人员编写的环境模型，程序运行时自动使用执行状态估计。信念程序动态地更新和查询信念状态，该信念状态捕获环境可能处于的可能状态。为了使验证，我们提出了认知霍尔逻辑的原因有关的可能的信念状态的信念程序的方式相同，经典的霍尔逻辑的原因有关的可能状态的程序。我们开发这些概念，定义一个简单的核心语言BLIMP的语义和程序逻辑。在一个案例研究中，我们展示了如何信念编程可以用来编写和验证控制器的火星极地着陆器在BLIMP。我们提出了一个实现的BLIMP称为CBLIMP和评估，以确定信念编程的可行性。
2021-01-12 cs.PL
Bonsai: Synthesis-Based Reasoning for Type Systems
我们描述的符号推理算法的类型系统的可执行模型，支持三个查询类型系统的设计者打算。首先，我们检查类型健全性错误，并合成一个反例程序，如果这样的错误被发现。其次，我们比较两个版本的类型系统，合成一个程序接受，但拒绝了另一个。第三，我们最小化合成反例程序的大小。这些算法象征性地评估类型检查器和解释器，产生表征在类型检查器和解释器中失败或成功的程序集的公式。然而，象征性地评估解释器带来了效率挑战，这是由于必须合并各种可能的输入程序的执行路径而引起的。我们的主要贡献是盆景树，一个新的象征性的表示程序和程序状态，解决这些挑战。Bonsai树根据逻辑约束对复杂的语法信息进行编码，从而实现更有效的合并。我们实现这些算法的盆景工具，类型系统设计师的助手。我们对Bonsai如何帮助测试和探索各种类型系统进行案例研究。Bonsai有效地合成了自动化工具无法访问的可靠性错误的反例，并且是第一个为最近发现的Scala可靠性错误SI-9633找到反例的自动化工具。
2017-08-01 cs.PL
Fixed Point Semantics for Stream Reasoning
Institute of Discrete Mathematics and Geometry（离散数学与几何研究所）；Vienna University of Technology（维也纳工业大学）
对输入数据流进行推理是人类智能的重要组成部分。在过去的十年中，{ \em流推理}已经成为人工智能社区中的一个研究领域，具有许多潜在的应用。事实上，通过谷歌和Facebook等服务提供的流数据的可用性越来越高，这就需要推理引擎来处理高速变化的数据。最近，基于规则的形式主义{ \em LARS}的答案集语义下的非单调流推理已经推出。从语法上讲，LARS程序是逻辑程序，具有否定，并结合了用于时间推理的运算符，最值得注意的是用于选择相关时间点的{ \em窗口运算符}。不幸的是，通过预先选择{ \em fixed}间隔用于程序的语义评估，LARS程序的刚性语义不够灵活，{ \em constructively}无法应对快速变化的数据依赖性。此外，我们表明，定义的答案集语义的LARS在FLP约简导致不良循环的理由类似于其他ASP扩展。本文解决了LARS的所有上述缺点。更确切地说，我们有助于流推理的基础，提供了一个完全灵活的变体LARS的操作不动点语义，我们表明，我们的语义是健全的和建设性的意义上说，答案集是自下而上的推导和自由的循环理由。
2020-05-17 cs.AI cs.CL cs.LO
S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs
众所周知，堆操作程序是很难推理的。我们提出了一种新的验证器堆操作程序称为S2 TD，它编码的程序系统的形式约束角子句（CHC）使用一种新的扩展分离逻辑（SL）与递归谓词和悬空谓词。S2 TD积极探索循环证明来解决路径爆炸问题。S2 TD区别于现有的基于CHC的验证程序，专注于堆操作程序，并采用循环证明来有效地验证或证伪它们与反例。与现有的基于SL的验证器相比，S2 TD精确地指定了解除分配的指针堆，以避免错误存在的推理中的误报。S2 TD已经使用来自SV-COMP存储库的一组全面的基准程序进行了评估。结果表明，S2 TD比最先进的程序验证器更有效，比大多数程序验证器更高效。
2022-09-19 cs.PL cs.SE
Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters
University of Southern California（南加州大学）
本研究针对LLM用于程序验证时语义推理机制不明的问题，提出两种激发抽象解释推理的提示策略，在SV-COMP基准的22个程序上评估了多款前沿LLM，分析了不变量可靠性与推理错误模式，为LLM与程序验证交叉研究提供了新方向。
2025-09-30 cs.LG cs.PL cs.SE
Evaluating Program Semantics Reasoning with Type Inference in System F
University of California, Davis（加州大学戴维斯分校）；University of Hong Kong（香港大学）
本文提出基于 System F 类型推断的 TF-Bench 及纯语义变体 TF-Bench_pure，并辅以鲁棒性与测试时推理指标，揭示先进 LLM 在真正程序语义推理上仍存在明显不足。
2025-10-20 cs.CL cs.PL cs.SE
L0-Reasoning Bench: Evaluating Procedural Correctness in Language Models via Simple Program Execution
NVIDIA（英伟达）
本文提出 L0-Bench 基准，通过合成 Python 函数执行轨迹评估语言模型的过程正确性，发现模型随步数增加而退化，并探索测试时扩展以改进 level-0 推理。
2025-04-10 cs.CL cs.PL
SPARK: Static Program Analysis Reasoning and Retrieving Knowledge
School of Information Technologies, University of Sydney（悉尼大学信息技术学院）；Department of Computer Science, Yonsei University（延世大学计算机科学系）；Qatar Computing Research Institute（卡塔尔计算研究所）
程序分析是一种不用执行程序就能对程序进行推理的技术，它在编译器、集成开发环境和安全性方面有各种应用。在这项工作中，我们提出了一个机器学习管道，诱导程序的安全分析器的例子。安全分析器根据我们的机器学习管道推导出的符号规则来确定程序是安全还是不安全。机器流水线分为两个阶段，包括一个递归神经网络（RNN）和一个将RNN转换为符号规则的提取器。为了评估学习的符号规则的质量，我们提出了一个基于采样的两个无限正则语言之间的相似性度量。我们使用真实世界的数据进行案例研究。在这项工作中，我们讨论了现有技术的局限性和未来可能的改进。结果表明，在有足够的训练数据和合理分布的程序路径的情况下，对数百万行代码的OpenJDK库进行符号安全规则推导是可行的。
2017-11-03 cs.AI cs.CR cs.PL
Beyond Either-Or Reasoning: Transduction and Induction as Cooperative Problem-Solving Paradigms
本文提出协作转换-归纳问题解决范式，通过交替使用转换与归纳推理模式，提升程序生成性能，其在三个PBE领域中均优于现有方法，生成更贴近真实行为的程序。
2026-08-05 cs.AI cs.LG cs.PL
CodeARC: Benchmarking Reasoning Capabilities of LLM Agents for Inductive Program Synthesis
Stanford University（斯坦福大学）；University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）；MIT（麻省理工学院）；Intel（英特尔）；Nanjing University（南京大学）
本文提出CodeARC评估框架与基准，通过交互式差分测试和迭代优化评估LLM智能体在归纳式程序合成任务中的推理能力，实验表明该任务极具挑战性且微调能显著提升性能。
2025-08-08 cs.AI cs.CL cs.LG
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
