Dafny as Verification-Aware Intermediate Language for Code Generation
Massachusetts Institute of Technology（麻省理工学院）；Amazon（亚马逊公司）
针对大语言模型生成代码易出错的问题，提出引导LLM先生成可自动验证的Dafny中间表示，验证通过后编译为目标语言，全程自然语言交互，在HumanEval基准上测试了原型性能。
2025-01-10 cs.AI cs.CL cs.LO
Ownership in low-level intermediate representation
针对低级程序验证中所有权信息缺失、指针无法用FOL抽象的问题，为类LLVM低级中间表示设计所有权语义，通过指针缓存减少地址映射维护，在SEABMC中实现后，C程序验证的SMT求解速度提升1.3x-5x。
2024-08-13 cs.PL cs.SE
Verification of High-Level Transformations with Inductive Refinement Types
像Rascal这样的高级转换语言包括用于操作大型抽象语法树的表达功能：第一类遍历，表达模式匹配，回溯和广义迭代器。我们提出了一个抽象的解释工具，Rabit的设计和实现，用于验证归纳类型和形状属性的转换写在这样的语言。我们描述了如何执行抽象解释的基础上操作语义，特别是集中在分析时所产生的挑战的表达遍历和模式匹配。最后，我们对Rabit进行了一系列转换（规范化、去糖、重构、代码生成器、类型推断等）。这表明我们可以有效地验证所述属性。
2018-09-17 cs.PL
Modular termination verification with a higher-order concurrent separation logic (Intermediate report)
我们报告的中间结果，我们的研究推理活性属性，除了深正确性的一个命令，并发程序设计语言与高阶存储。目前，我们集中在一个特定的活性属性，即终止。通过保证终止性，我们可以将部分正确性的陈述加强为完全正确性。这是通过将终止性转换为安全属性的经典方法来实现的。特别是，我们扩展的程序设计语言考虑与调用权限，这已被证明，使模块化的推理终止。添加原子块是为了增加我们基于调用权限的方法的表现力。我们的工作建立在Iris --一个基础的、机器检查的、高阶并发分离逻辑框架--之上，而不修改它。有了这些补充，我们就能够模块化地推理并发但非阻塞算法的终止。我们对正在考虑的程序设计语言的添加保留了Iris对帮助和预言进行推理的能力。作为一个例子，我们将当前的系统应用于现有的无锁并发堆栈的案例研究，并在Iris中得到了证明。最后，我们概述了扩展阻塞并发方法的后续步骤。
2022-12-28 cs.LO cs.PL
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)
本文提出基于前向模拟和 Isabelle 自动证明的方法，为验证器前端到 IVL 的翻译提供形式化可靠性保证，并在 Viper 到 Boogie 的实现上验证有效性。
2024-05-09 cs.PL
Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis (Extended Version)
为了验证混合系统，我们扩展了抽象解释。摘要抽象在混合系统的验证方法中扮演着重要的角色，但对于常微分方程定义的连续动态的抽象需要特别注意。我们应用Cousot和Cousot的抽象解释框架的混合动力系统，几乎是因为它是，通过把连续动态无穷小离散跳跃的无限迭代。这种扩展遵循了Suenaga，Hasuo和Sekine最近的工作路线，其中演绎验证扩展为混合系统：1）为无穷小值引入常数dt; 2）采用Robinson的非标准分析（NSA）来定义数学上严格的语义。我们的理论结果包括健全性和终止通过统一加宽运营商和我们的原型实现成功地验证了一些基准的例子。
2015-11-03 cs.PL
Automatic Verification of Erlang-Style Concurrency
提出了一种自动验证Erlang式高阶并发程序安全性的方法。受Core Erlang的启发，我们引入了Lambda-Actor，这是一种具有模式匹配代数数据类型的原型函数式语言，并增加了进程创建和异步消息传递原语。我们正式的抽象模型的λ-演员程序称为演员通信系统（ACS），它有一个自然的解释为一个矢量加法系统，其中一些验证问题是可判定的。我们给出了一个参数化的抽象解释框架，并使用它来构建一个多时间可计算的，基于流的，抽象语义的Lambda-Actor程序，然后我们使用它来引导ACS的建设，从而得出一个更准确的输入程序的抽象模型。我们已经构建了Soter，一个验证方法的工具实现，从而获得了第一个全自动的，无限状态的Erlang核心片段的模型检查器。我们发现，在实践中，我们的抽象技术是准确的，足以验证一个有趣的范围内的安全属性。虽然ACS的可覆盖性问题是Expspace完备的，但Soter可以非常有效地分析这些验证问题。
2013-03-09 cs.PL
Proceedings of the Fourth International Workshop on Verification and Program Transformation
本卷包含2016年4月2日在荷兰埃因霍温举行的第四届验证和程序转换国际研讨会（VPT 2016）上提交的论文的修订版。该研讨会是欧洲软件理论与实践联合会议（ETAPS 2016）的一项活动。VPT研讨会的目的是提供一个论坛，来自程序转换领域和程序验证领域的人们可以卓有成效地交换意见，并对这两个领域之间的相互作用有更深入的了解。最近在这些领域发表的研究论文表明，相互作用是非常有益的，实际上是双向的。在一个方向上，在程序转换领域中开发的方法和工具，例如部分演绎，部分求值，折叠/展开转换和超级编译，都已成功地应用于系统的验证，特别是无限状态和参数化系统的验证。在另一个方向，在程序验证，如模型检验，抽象解释，SAT和SMT解决，自动定理证明，已被用来增强程序转换技术，从而使这些技术在实践中更强大和有用的方法。
2016-07-06 cs.PL cs.SE
Proceedings of the Third International Workshop on Verification and Program Transformation
本卷包含2015年4月11日在英国伦敦举行的第三届验证和程序转换国际研讨会（VPT 2015）上发表的论文。讲习班的前两届讲习班分别于2013年在圣彼得堡（俄罗斯）和2014年在维也纳（奥地利）举行。这些论文表明，在程序转换领域中开发的方法和工具，如部分求值和折叠/展开转换，以及超级编译，可以应用于软件系统的验证。他们还展示了一些程序验证方法，如模型检验技术，抽象解释，SAT和SMT解决，自动定理证明，可以用来增强程序转换技术，从而使这些技术在实践中更强大和有用。
2015-12-06 cs.LO cs.PL cs.SE
Analysis and Transformation Tools for Constrained Horn Clause Verification
已经开发了几种技术和工具，用于验证表示为Horn子句的属性，并在背景理论（CHC）上进行约束。目前的CHC验证工具实现复杂的算法，往往局限于某些子类的CHC问题。我们在这项工作中的目的是调查使用的组合现成的技术从文献中的约束逻辑程序（CLP）的分析和改造，以解决具有挑战性的CHC验证问题。我们发现，许多问题可以解决使用的工具组合的基础上众所周知的技术，从抽象的解释，语义保持转换，程序专业化和问答转换。这提供了深入了解的自动，更一般的CHC验证工具的基础上的组件库的设计。
2014-05-15 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 Linear First-Order Functional Intermediate Language for Verified Compilers
我们提出了线性一阶中间语言IL验证编译器。IL是一种函数式语言，可以调用非确定性环境。我们给IL条款的第二个，命令式语义解释，并获得一个寄存器转移语言。对于命令式解释，我们建立了活变量的概念。基于活变量，我们制定了一个可判定的属性称为一致性，确保功能和命令的解释一个术语相吻合。我们制定了一个寄存器分配算法的IL，并证明其正确性。该算法将一个函数式IL程序转换为一个等价的命令式IL程序。正确性来自于这样一个事实，即算法在一致地重命名局部变量后达到了一个连贯的程序。我们证明了初始程序中的最大活变量数限制了最终相干程序中不同变量的数量。整个开发都在Coq中正式化。
2015-06-04 cs.PL
A Deductive Verification Framework For Higher Order Programs
在本报告中，我们介绍了为我们的APDC（Area Prática de Desenvolvimento Curriculum）课程研究项目开展的初步工作。这个项目的主要目标是开发一个框架，在Why3工具之上，用于验证有效的高阶程序。我们使用去功能化作为从高阶OCaml实现到一阶OCaml实现的中间转换。我们翻译的目标是WhyML，Why3的程序设计语言。我们相信去功能化可以是一个有趣的路线，高阶程序的自动验证，因为人们可以采用现成的自动程序验证器来证明所生成的一阶程序的正确性。这份报告还向读者介绍了演绎程序验证的主题，以及用于证明高阶有效程序的一些工具和概念。
2020-11-28 cs.LO cs.PL
Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses
本文提出一种结合自动机和逻辑的自动验证技术，通过knitted-tree编码将程序执行映射为单一树结构，并利用约束Horn子句刻画其组合性质，将验证简化为求解CHC可满足性问题，广泛适用于树操作程序的多种验证任务。
2024-10-12 cs.PL
Towards a Deductive Verification Infrastructure for Weighted Programming
RWTH Aachen University（亚琛工业大学）
该研究针对加权程序构建了演绎验证框架，证明了核心命令翻译、证明规则编码及量词消去的可靠性，基于Caesar验证器的原型可验证多类定量与符号模型相关案例。
2026-08-20 cs.PL
SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks
LMU Munich（慕尼黑大学）；Masaryk University（马萨里克大学）
SV-LIB 1.0提出了一种用于软件验证任务的标准交换格式，支持程序、规范和验证见证的表示与交换，旨在提升跨语言验证工具的兼容性与重用性。
2025-11-26 cs.PL cs.SC 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
Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation
这些会议记录包括在第九届验证和合成霍恩条款研讨会和第十届验证和程序转换国际研讨会上提交的选定论文，这两个研讨会都隶属于ETAPS 2022。许多感兴趣的程序验证和综合问题可以直接使用Horn子句建模，CLP和CAV社区的许多最新进展都集中在有效地解决Horn子句提出的问题上。HCVS系列研讨会旨在汇集在约束/逻辑编程社区工作的研究人员（例如，ICLP和CP），程序验证（例如，CAV、TACAS和VMCAI）和自动演绎（例如，CADE，IJCAR），关于基于Horn子句的分析、验证和综合的主题。这些团体在不同的时期从不同的角度倡导关于核查和综合的霍恩条款，组织HCVS是为了促进互动和富有成效的经验交流和整合。VPT研讨会的目的是汇集在程序验证和程序转换领域工作的研究人员。这两个领域之间有很大的潜力进行有益的互动，因为：1）一方面，在程序转换领域开发的方法和工具，如部分评估，折叠/展开转换和超级编译，都已成功应用于验证无限状态和参数化系统。2)另一方面，模型检验，抽象解释，SAT和SMT解决和自动定理证明已被用来加强程序转换技术。此外，程序转换工具的正式认证，如自动重构工具和编译器，最近吸引了相当大的兴趣，提出了重大挑战。
2022-11-19 cs.LO cs.PL cs.SC
A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)
RWTH Aachen University（亚琛工业大学）；Saarland University（萨尔兰州立大学）；University College London（伦敦大学学院）；Technical University of Denmark（丹麦技术大学）
本文提出一个面向离散概率程序的定量验证基础设施，类似Boogie，采用实值逻辑和中间验证语言，支持期望性质验证，并基于SMT实现自动验证多种基准。
2026-09-24 cs.PL
CANAL: A Cache Timing Analysis Framework via LLVM Transformation
一个统一的建模框架的非功能特性的程序是必不可少的软件分析和验证的研究，因为它减少了负担，个人研究人员实施新的方法和比较现有的方法。我们提出了CANAL，一个框架，通过转换其中间表示LLVM编译器中的程序的缓存行为建模。CANAL在这些变量上插入辅助变量和指令，以允许标准验证工具处理一类新的高速缓存相关属性，例如，用于计算最坏情况下的执行时间和检测侧通道泄漏。我们使用三种验证工具：KLEE，SMACK和Crab-llvm证明了CANAL的有效性。我们确认我们的缓存模型的准确性，通过比较与CPU周期准确的模拟结果GEM 5。CANAL可以在GitHub和YouTube上找到。
2018-07-09 cs.CR cs.PL cs.SE
Decidable Verification of Uninterpreted Programs
我们研究的问题是完全自动验证未解释的程序--程序工作在任意的数据模型，提供了一个解释的常数，功能和程序使用的关系。验证问题询问给定的程序是否满足使用无量词公式编写的后置条件，在最终状态上具有相等性，没有提供循环不变式，合同等。我们证明了这个问题在一般情况下是不可判定的。本文的主要贡献是一个子类的程序，称为一致的程序，承认可判定的验证，并可以决定在PSPACE。然后，我们扩展这类程序的程序，是$k$ -连贯的，其中$k \in \mathbb{N}$，通过（自动）添加$k$鬼变量和分配，使它们连贯。我们还扩展了可判定性的结果与递归函数调用的程序，并证明了几个不可判定性的结果，表明为什么我们的限制，以获得可判定性似乎是必要的。
2020-08-26 cs.FL cs.LO cs.PL
Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
本文为含循环、连续分布和条件化的概率程序验证奠定基础，通过黎曼和近似积分实现SMT不变量验证，并证明收敛性与完备性，且可在现有工具中应用。
2025-02-26 cs.LO cs.PL
Practical Formal Verification for MLIR Programs
Georgia Institute of Technology（佐治亚理工学院）；Colorado State University（科罗拉多州立大学）
本文提出通过语义等价性验证MLIR程序转换的正确性，采用混合具体-符号解释方法，实现线性时间等价性检测，并验证了AMD MLIR-AIR、MLIR-AIE工具链及mlir-opt在多个基准测试中的正确性。
2026-05-01 cs.PL
Automatic Probabilistic Program Verification through Random Variable Abstraction
最弱预期望演算已被证明是分析概率和不确定性规划定量性质的成熟理论。我们提出了一个自动的方法证明定量线性性质的任何可数状态空间使用迭代向后不动点计算的一般框架中的抽象解释。为了完成这一任务，我们提出了随机变量抽象（RVA）的技术，我们还假设了一个充分条件，实现精确的不动点计算的抽象域。我们的方法的可行性示出了两个例子，一个获得的概率程序的预期运行时间，和其他的赌博策略的预期收益。我们的方法适用于一般的保护概率和不确定性的过渡系统，而不是普通的pGCL程序，使我们能够很容易地模拟广泛的系统，包括分布式的和非结构化的程序。我们提出了该程序的操作和最弱前提语义，并证明了它的等价性。
2010-06-26 cs.LO cs.PL
Formalization of Quantum Intermediate Representations for Code Safety
量子中间表示（QIR）是微软开发的，基于LLVM的量子程序编译器中间表示。QIR旨在为量子程序编译器提供一个独立于前端语言和后端硬件的通用解决方案，从而避免中间表示和编译器的重复开发。由于QIR仍在开发中，它是用自然语言描述的，缺乏正式的定义，导致其解释模糊不清，实现量子功能时缺乏严谨性。本文给出了QIR的数据类型和指令集的形式化定义，旨在为QIR中的操作和中间代码转换提供正确性和安全性保证。为了验证我们的设计，我们展示了一些不安全的QIR代码样本，其中错误可以通过我们的正式方法检测到。
2023-03-25 cs.PL quant-ph
An encoding of array verification problems into array-free Horn clauses
自动验证程序的安全属性是困难的，如果程序作用于数组或其他形式的映射，则更难。存在许多方法来验证程序操作上的布尔和整数值（例如抽象的解释，反例引导的抽象细化使用插值），但转置它们数组属性已充满了困难。与大多数以前的方法相比，我们不引入一个新的抽象域或一个新的插值过程数组。相反，我们生成一个抽象的标量问题，并将其提供给一个预先存在的求解器，与可调precision.Our转换的问题表示使用霍恩条款，一个共同的格式与明确和明确的逻辑语义验证问题。我们的编码的一个重要特点是，它创建了一个非线性的霍恩问题，与树展开，即使下面的“平坦”的控制图结构通常会产生一个线性的霍恩问题，与线性展开。也就是说，我们的编码不能表示成另一个控制流图问题的编码，并真正利用霍恩子句格式的能力。我们说明了我们的方法与选择排序的功能正确性的完全自动化的证明。
2015-09-30 cs.LO cs.PL
Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
Uppsala University（乌普萨拉大学）；KTH Royal Institute of Technology（皇家理工学院）；Intel Labs（英特尔实验室）
本文提出了一种面向符号执行的理论，用于在可信系统中自动验证二进制代码的功能和非功能属性，通过HOL4定理证明器实现了该理论，并展示了其在RISC-V和ARM Cortex-M0上的应用效果。
2026-01-13 cs.CR cs.LO cs.PL
