Separation Logic for Verifying Physical Collisions of CNC Programs
SLING AI Inc.（SLING AI 公司）
本文提出了一种形式验证框架，将CNC工作空间概念化为空间堆，利用分离逻辑验证安全性和物理碰撞，通过形式三元组检测逻辑空间竞赛，扩展到协作环境并支持多轴运动学。
2026-05-20 cs.LO cs.SE
Experience Report on Formally Verifying Parts of OpenJDK's API with KeY
软件的演绎验证尚未进入行业，因为复杂性和可扩展性问题需要高度专业的专家。然而，长期的观点是开发验证工具，帮助工业软件开发人员更快，更容易地找到软件系统中的错误或瓶颈。KeY项目构成了一个用于指定和验证软件系统的框架，旨在使形式化验证工具适用于主流软件开发。为了帮助KeY的开发人员、用户和演绎验证社区，我们从用户的角度总结了使用KeY 2.6.1指定和验证真实世界Java代码的经验。为此，我们集中讨论OpenJDK 6的Collections-API的部分内容，其中存在非正式规范。当我们描述我们如何桥接非正式和正式规范时，我们也展示了我们遇到的伴随的挑战。我们的经验是，（a）原则上，演绎验证类API代码库是可行的，但需要很高的专业知识，（b）为现有的代码库开发正式的规范仍然是出了名的困难，（c）在Java中的某些语言结构的规格是具有挑战性的工具建设者。我们在指定OpenJDK 6的部分方面的初步努力构成了未来研究案例研究的垫脚石。
2018-11-27 cs.LO cs.PL cs.SE
Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation
Singapore University of Technology and Design（新加坡科技与设计大学）
信息物理系统（CPS），它集成了算法控制与物理过程，通常由物理分布的组件通过网络进行通信。这种CPS中的故障或受损组件可能导致代价高昂的后果，特别是在公共基础设施的背景下。在这篇简短的论文中，我们认为构建CPS所表现出的物理行为的不变量（或模型）的重要性，其动机是它们的应用程序的控制，监控和认证的组件。为了实现这一目标，尽管CPS具有固有的复杂性，我们提出了一种学习不变量的新技术，该技术将机器学习与突变测试的想法相结合。我们提出了一个水处理系统的初步研究，表明这种方法的有效性，提出了建立信心的不变量的正确性的策略，然后总结了一些研究问题和我们正在采取的步骤来调查他们。
2016-09-06 cs.LG cs.LO cs.SE
Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK
secunet Security Networks AG（secunet安全网络股份公司）；International Center for Computational Logic, Technical University Dresden（德累斯顿工业大学国际计算逻辑中心）
针对LLM生成代码正确性无法被固有信任的问题，本文提出Marmaragan工具，利用LLM生成SPARK注释以实现代码形式化验证，其结合GPT-4o在基准测试中为50.7%的案例生成正确注释，为LLM与形式化验证结合奠定基础。
2025-02-11 cs.AI cs.SE
ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation
在这项工作中，我们描述和评估了第一个模型检查器，用于通过Jimple中间表示来验证Kotlin程序。该验证器名为ESBMC-Jimple，构建在基于高效SMT的上下文边界模型验证器（ESBMC）之上。它使用Soot框架来获得Jimple IR，代表Kotlin源代码的简化版本，每条指令最多包含三个操作数。ESBMC-Jimple将Kotlin源代码与标准Kotlin库的模型一起处理，并检查一组安全属性。实验结果表明，ESBMC-Jimple可以正确验证文献中的一组Kotlin基准测试，并且与最先进的Java字节码验证器相比具有竞争力。可在https://youtu.be/J6WhNfXvJNc上获得演示。
2022-07-20 cs.SE
Verified Rust Monitors for Lola Specifications
网络物理系统的安全取决于其监测机制的正确性。如果监视器的规范是手动实现的或由不可靠的软件解释的，则这是有问题的。我们提出了一个验证编译器，它将基于流的监控语言Lola中的规范转换为Rust中的实现。生成的代码包含验证注释，使Viper工具包能够自动证明功能正确性，不存在内存错误，并保证终止。编译器基于规范的依赖性分析，并行化监视器中不同流的评估。我们提出了令人鼓舞的实验结果与显示器规格在文献中找到。对于每一个规范，我们的方法都能够产生正确性证明或发现规范中的错误。
2020-12-15 cs.FL cs.SE
Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity
利用智能合约漏洞可能会带来灾难性的后果，例如损失价值数百万英镑的加密资产。形式化验证是识别漏洞并证明漏洞已被修复的有用工具。在本文中，我们使用Solid语言及其区块链对Solidity和以太坊区块链进行了形式化;通过对Solidity程序进行解释/去糖来获得Solid程序。我们做了一些抽象，过度近似Solidity/Ethereum的行为方式。基于这种形式化，我们创建了Solidifier：Solidity的有界模型检查器。它将Solid翻译成Boogie，一种中间验证语言，稍后使用Corral进行验证，这是Boogie的有界模型检查器。与该领域的许多工作不同，我们不会试图找到可能导致漏洞的特定行为/代码模式。相反，我们提供了一个工具来查找错误/坏状态，即不符合开发人员意图的程序状态。这种糟糕的状态，无论是否是漏洞，都可能通过执行特定的已知代码模式或通过未预期的行为达到。
2020-02-07 cs.CR cs.LO cs.PL
Uncovering Systematic Failures of LLMs in Verifying Code Against Natural Language Specifications
University of Sydney（悉尼大学）
本文揭示了大语言模型在判断代码是否符合自然语言需求时存在系统性误判，复杂提示反而加剧误判率，并提出两种改进提示策略以缓解该问题。
2025-08-17 cs.AI cs.SE
Verifying Autoware Controller Node by Combining Model Verification and Runtime Monitoring
Japan Advanced Institute of Science and Technology（日本科学技术大学）
针对Autoware轨迹跟踪控制节点，提出结合dL形式化模型验证与运行时监控的混合验证方法，经KeYmaera X证明模型属性，实验验证其跟踪精度，为自主驾驶系统验证提供有效方案。
2026-10-14 cs.SE
Verifying Time Complexity of Binary Search using Dafny
形式化软件验证技术被广泛用于描述和证明程序的功能正确性。然而，非函数性质，如时间复杂度，通常是用笔和纸来完成的。在大规模复杂系统中，在时间复杂度方面低效的代码可能导致大量的性能问题。我们提出了一个概念证明使用Dafny验证工具来指定和验证二叉搜索的最坏情况下的时间复杂度。这种方法也可以用于学术目的，作为教授算法和复杂性的新方法。
2021-08-06 cs.SE
ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
University of Cambridge（剑桥大学）；Amazon Web Services（亚马逊云科技）
ATLAS通过生成验证代码提升LLM在形式验证领域的性能，其在DafnyBench和DafnySynthesis上的表现显著提升。
2026-02-02 cs.SE
TransferFuzz: Fuzzing with Historical Trace for Verifying Propagated Vulnerability Code
针对代码复用导致漏洞传播但现有方法无法验证其在新环境中可触发的问题，提出TransferFuzz框架，通过提取基础二进制文件的历史轨迹并结合密钥字节引导变异与嵌套模拟退火算法，实现高效验证，速度为现有方法的2.5-26.2倍，还扩展了15个漏洞的受影响范围。
2024-11-27 cs.SE
Are Users More Willing to Use Formally Verified Password Managers?
本研究通过两项实验（15人形成性研究及200人定量研究）探究用户对形式化验证密码管理器的态度，发现用户视其为可取，并提出三项沟通改进建议。
2025-09-07 cs.CR cs.HC cs.LO
From Reading Code to Reading Spec: A Verified Layer for LLM-Driven Codebase Maintenance
Portland State University（波特兰州立大学）；Clemson University（克莱姆森大学）
针对LLM生成代码增加维护负担的问题，提出PROOF方法，通过结构化规范间接管理代码库，验证语义等价性并同步更新，实验证明其有效性。
2026-09-09 cs.CL cs.SE
The AutoProof Verifier: Usability by Non-Experts and on Standard Code
形式化验证工具通常是由专家为专家开发的;因此，对于没有什么形式化方法经验的程序员来说，它们的可用性可能会受到严重的限制。在本文中，我们讨论了这种普遍现象，参考AutoProof：一个工具，可以验证面向对象软件的完整功能的正确性。特别是，我们提出了我们的经验，使用AutoProof在两个对比的情况下，代表非专家的用法。首先，我们讨论其可用性的学生在研究生课程的软件验证，谁的任务是验证各种排序算法的实现。其次，我们评估其可用性验证代码开发的编程作业的本科课程。第一个场景代表了非专业人士的可用性;第二个场景代表了“标准代码”的可用性，开发时没有考虑到完整的功能验证。我们报告我们的经验和教训，从中我们得出一些一般性的建议，进一步发展的核查工具，提高其可用性。
2015-08-17 cs.HC cs.LO cs.SE
VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models
本文提出VECOGEN工具，结合大型语言模型与形式化验证，通过接收形式化规范、自然语言规范和测试用例，自动生成并迭代改进C程序，在Codeforces的15个问题中成功解决13个，验证了该方法在安全关键应用中的有效性。
2025-04-07 cs.SE
UTC Time, Formally Verified
本文介绍了基于Coq开发的时间转换验证库FV Time，其实现了现有库普遍缺失的闰秒功能，还产出了可复用的数值精化包与有限域自动证明策略，阐释了Coq软件验证方法论。
2023-12-13 cs.SE
Automated Testing and Repair for Verified Compilers Generated by a Coding Agent
National University of Singapore（新加坡国立大学）；Massachusetts Institute of Technology（麻省理工学院）
该研究针对编码智能体生成的验证编译器，提出了基于智能体的自动化测试与修复系统，经评估其在Axon编译器上无奖励黑客攻击问题，可有效开展测试与修复。
2026-08-03 cs.SE
From Event-B to Verified C via HLL
这项工作解决了一个事件B模型的C代码通过一个中间形式语言，HLL的正确翻译。正确性的证明遵循两个主要步骤。首先，将Event-B模型的最终细化（包括不变量）转换为HLL。在这一点上，额外的属性（例如，无死锁性、活跃性等）添加到HLL模型中。在HLL级别上对不变量和附加属性的证明保证了翻译的正确性。其次，C代码是从HLL模型自动生成的，用于大多数系统功能，并手动为其余的;在这种情况下，HLL模型提供正式的合同给软件开发人员。C代码与HLL模型的等价性证明保证了代码的正确性。
2016-10-24 cs.SE
Debug like a Human: A Large Language Model Debugger via Verifying Runtime Execution Step-by-step
University of California, San Diego（加利福尼亚大学圣迭戈分校）
本文提出LDB调试框架，将程序分割为基本块并跟踪运行时中间变量值，使LLMs能逐块验证代码正确性并定位错误，在多个基准上提升调试性能最高达9.8%。
2024-06-06 cs.AI cs.CL cs.SE
DeepSaucer: Unified Environment for Verifying Deep Neural Networks
Hitachi, Ltd.（日立有限公司）；University of Southampton（南安普顿大学）
近年来，已经开发了许多用于验证DNN的方法。由于这些方法的方法不同，有自己的局限性，我们认为，一些验证方法应适用于开发DNN。要将许多方法应用于DNN，需要转换DNN的实现或验证方法，以便一个在相同的环境中运行。由于这些翻译非常耗时，因此提出了一种名为DeepSaucer的实用工具，该工具有助于保留和重用DNN，验证方法及其环境的实现。在DeepSaucer中，加载DNN、运行验证方法和创建其环境的代码片段被保留并作为软件资产重用，以降低验证DNN的成本。DeepSaucer的可行性通过在Anaconda的基础上实现来证实，Anaconda为加载DNN和运行验证方法提供了虚拟环境。最后通过实例验证了DeepSaucer的有效性。
2018-11-09 cs.LG cs.SE
Verifying Controllers with Convolutional Neural Network-based Perception: A Case for Intelligible, Safe, and Precise Abstractions
University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）；Coordinated Science Laboratory（协调科学实验室）
针对CNN感知模型安全性分析困难的问题，提出一种从系统级安全需求和下游模块推断可理解且安全抽象的技术，并在高保真仿真中验证了其能有效权衡安全、规模与精度并指导极端情况搜索。
2021-11-10 cs.RO cs.SE
WybeCoder: Verified Imperative Code Generation
CERMICS, ENPC, Institut Polytechnique de Paris, CNRS（CERMICS，ENPC，巴黎理工学院，CNRS）；Computer Lab, University of Cambridge（剑桥大学计算机实验室）；Korea Institute for Advanced Study（韩国高级研究院）；FAIR, Meta（FAIR，Meta）；University College London（伦敦大学学院）
WybeCoder 提出了一种验证性 imperative 代码生成框架，通过证明与生成同步的方式，实现代码、不变式和证明的共同进化，提升了复杂算法的验证效率。
2026-04-14 cs.AI cs.SE
CodeDPO: Aligning Code Models with Self Generated and Verified Source Code
CodeDPO 提出将偏好学习融入代码生成，通过自生成与验证机制和 PageRank 启发式算法构建基于正确性与效率的偏好数据集，在多个基准上显著提升代码模型的正确性和运行效率。
2025-06-03 cs.SE
CLEVER: A Curated Benchmark for Formally Verified Code Generation
UT Austin（得克萨斯大学）；Amazon（亚马逊）；Caltech（加州理工学院）
CLEVER是一个包含161个问题的精选基准，用于Lean中端到端验证代码生成，通过避免测试用例监督和规范泄露，评估少样本与智能体方法，发现现有方法难以完全验证，成为程序合成与形式推理的前沿挑战基准。
2025-10-23 cs.AI cs.LG cs.LO
Formally Verified Code Synthesis for Structured Data Translation in a Medical Internet of Things
Computer Science Laboratory, SRI International（SRI国际计算机科学实验室）
提出一种基于LLM的进化代码合成系统，集成形式化验证步骤，用于医疗物联网中结构化数据翻译，确保生成代码满足预定义需求，并以脉搏血氧仪集成案例展示其低开销生成正确翻译的能力。
2026-06-23 cs.AI cs.NE cs.SE
PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C
提出PyVeritas框架，利用LLM将Python转换为C，结合有界模型检验和基于MaxSAT的故障定位，实现Python代码的形式化验证与错误定位，转换准确度达80-90%。
2025-08-11 cs.AI cs.SE
Verifiable Source Code Documentation in Controlled Natural Language
ETH Zurich（苏黎世联邦理工学院）；University of Chile（智利大学）
编写关于软件内部的文档很少被认为是一种有价值的活动。当软件在多开发人员环境中不断发展时，这是非常耗时的，并且产生的文档是脆弱的。不幸的是，传统的编程环境对文档的编写和维护支持不足。由于缺乏软件结构文档，对软件产品的整体质量产生了负面影响，因此后果是严重的。我们表明，使用受控的自然语言与推理机和查询引擎是一种可行的技术，用于验证文档和源代码的一致性和准确性。使用ACE，一个国家的最先进的控制自然语言，我们提出了积极的成果的可理解性和一般的可行性创建和验证文档。作为一个案例研究，我们使用自动文档验证来识别和修复一个重要软件架构中的严重缺陷。此外，用户实验表明，我们的语言是更快，更容易学习和理解比其他形式语言的软件文档。
2013-11-12 cs.AI cs.CL cs.HC
Towards Verified Code Reasoning by LLMs
University of Texas at Austin（德克萨斯大学奥斯汀分校）；Google DeepMind（谷歌DeepMind）；Google（谷歌）；Meta Platforms（元平台）
针对大语言模型代码推理结果不可靠、需人工核验的问题，本文提出结合形式化表示提取、形式化验证与程序分析工具的自动校验方法，在基准测试中有效验证了智能体推理并识别错误判断。
2025-11-13 cs.LG cs.SE
