Formal Semantics and Formally Verified Validation for Temporal Planning
Techniche Universität München（慕尼黑工业大学）；King’s College London（伦敦国王学院）
我们提出了一个简单而简洁的语义时间规划。我们的语义开发和形式化的逻辑的互动定理证明伊莎贝尔/HOL。我们从这些语义的验证算法的时间规划和显示，使用Isabelle/HOL的正式证明，该验证算法实现我们的语义。我们通过实验评估我们验证的验证算法，并表明它是实用的。
2022-03-25 cs.AI cs.LO
Formally Verified Certification of Unsolvability of Temporal Planning Problems
本文提出将时序规划问题编码为时间自动机网络，结合模型检查器与经 Isabelle/HOL 形式化验证的证书检查器，为不可解性结论提供高可信认证。
2025-10-19 cs.AI cs.LO
A formally verified proof of the prime number theorem
1896年由阿达玛和德·拉·瓦莱·普桑独立建立的素数定理断言，正整数中素数的密度渐近于1 / ln x。虽然他们的证明认真使用的方法复杂的分析，小学的证明提供了塞尔伯格和埃尔德奥斯在1948年。我们描述了一个正式验证版本的Selberg的证明，获得使用伊莎贝尔证明助手。
2006-04-06 cs.AI cs.LO cs.SC
A formally verified compiler back-end
本文描述了一个从Cminor（一种简单的命令式中间语言）到PowerPC汇编代码的编译器后端的开发和形式化验证（语义保持的证明），使用Coq证明助手对编译器进行编程并证明其正确性。这样的验证编译器是有用的，在形式化的方法应用于关键软件的认证的上下文中：编译器的验证保证了在源代码上证明的安全属性也适用于可执行的编译代码。
2009-11-14 cs.LO cs.PL
Duality theory in linear optimization and its extensions -- formally verified
Institute of Science and Technology Austria（奥地利科学技术研究所）
本文通过形式化证明，扩展了Farkas定理至线性有序域，并探讨了允许系数取无限值的对偶理论扩展。
2026-03-06 cs.LO math.OC
Formally Verified Approximate Policy Iteration
Technische Universität München（慕尼黑工业大学）；King’s College London（伦敦国王学院）
本文用 Isabelle/HOL 形式化验证因子 MDP 上的近似策略迭代算法，并将其精化为可执行实现，同时开发线性规划解认证软件以验证其实用性。
2024-06-11 cs.AI cs.LO
Plotting in a Formally Verified Way
计算机代数系统的一个非常宝贵的特性是它们能够绘制函数图。不幸的是，当人们试图设计一个数学函数库时，由于该用例固有的准确性问题，此功能通常会不足，产生不正确和潜在的误导性图。本文研究了情节正确的含义以及如何形式化地验证这一属性。Coq的证明助手，然后变成一个工具，用于绘制函数图使用可靠的多项式近似。此功能作为CoqInterval库的一部分提供。
2021-08-06 cs.LO cs.SE
A formally verified proof of the Central Limit Theorem
我们描述了一个证明的中心极限定理，已正式核实的伊莎贝尔证明助手。我们的形式化的基础上，并扩展伊莎贝尔的图书馆分析和测量理论的概率。该定理的证明使用特征函数，这是一种傅立叶变换，以证明，在适当的假设下，随机变量的总和弱收敛到标准正态分布。我们还讨论了支持正式化的库和基础设施，并反思了我们从这一努力中吸取的一些教训。
2017-02-01 cs.LO cs.MS math.PR
Certified Knowledge Compilation with Application to Formally Verified Model Counting
针对知识编译输出缺乏正确性保证的问题，提出分区操作图（POGs）及CPOG证明框架，并开发基于D4的生成与验证工具链及Lean 4形式化验证的模型计数器，构成首个形式化验证的模型计数工具链。
2025-01-22 cs.LO
A Formally Verified Lightning Network
本文利用 Why3 平台对闪电网络进行形式化验证，首次提供机器可检查的证明，证明其在所有场景下均能保护诚实用户资金安全。
2025-03-10 cs.CR cs.LO
TRX: A Formally Verified Parser Interpreter
语法分析是计算机科学中的一个重要问题，然而令人惊讶的是，很少有人关注它的形式化验证。在本文中，我们提出了TRX：解析器解释器正式开发的证明助手Coq，能够产生正式正确的解析器。我们正在使用解析表达式语法（PEG），一种形式主义，基本上代表递归下降解析，我们认为这是一个有吸引力的替代上下文无关文法（CFG）。从这种形式化中，我们可以提取出一个任意PEG语法的解析器，保证完全正确，即，所得到的解析器在其语法和PEG的语义方面是终止的和正确的;这两个属性在Coq中被正式证明。
2011-06-22 cs.FL cs.LO cs.PL
DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments
Mathematical Sciences Institute, Australian National University（澳大利亚国立大学数学科学学院）；Faculty of Information Technology, Monash University（蒙纳士大学信息技术学院）
本文通过序数赋值形式化验证皮亚诺算术一致性的构造性证明，并使用Coq定理证明器验证所有结果。
2026-02-28 cs.LO
Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified
本文在Lean 4中形式化验证了Seymour定理的正则拟阵组合方向，开发了相关矩阵与拟阵库，适用于有限秩且底集可能无限的情形。
2025-09-24 cs.LO math.CO
Dynamic Fault Trees Analysis using an Integration of Theorem Proving and Model Checking
动态故障树（DFTs）已成为一个重要的工具，捕捉系统故障的动态行为。然后，这些DFT定性和定量分析，使用随机或代数方法来判断给定系统的故障特征的子组件的故障。模型检验最近已被提出来进行故障分析的系统使用DFT的动机，以提供一个严格的故障分析的安全关键系统。然而，模型检验还没有被用于DFT的定性分析和约简算法中使用的模型检验通常没有正式验证。而且，分析时间随着状态数的增加呈指数增长。这些问题限制了模型检验在分析安全关键领域中使用的复杂系统时的有用性，在安全关键领域中，分析的准确性和完整性是最重要的。为了克服这些局限性，我们提出了一个全面的方法来进行定性和定量分析的DFT定理证明和模型检验为基础的方法集成。为此，我们形式化的所有基本的动态故障树门使用高阶逻辑的代数方法的基础上，并正式验证了一些简化属性。这种形式化允许我们使用定理证明器正式验证原始DFT和缩减DFT之间的等价性，并进行定性分析。然后，我们使用模型检验进行定量分析的正式验证减少DFT。我们应用我们的方法，以五个基准和结果表明，正式验证减少DFT分析使用模型检验与多达6倍少的状态和高达133000倍的速度。
2017-12-07 cs.LO
(Nearest) Neighbors You Can Rely On: Formally Verified k-d Tree Construction and Search in Coq
本文使用Coq证明助手形式化验证了k-d树的构建与K近邻搜索算法，提出了一种基于列表排列概念的直观方法来指定这些算法的属性。
2023-11-18 cs.CG cs.LO
Formally Verified Trades in Financial Markets
我们介绍了一个分析金融市场交易的正式框架。如今，所有大型交易所都使用计算机算法来匹配买入和卖出请求，这些算法必须遵守某些监管准则。例如，市场监管机构强制要求交易所产生的匹配应该是公平的、统一的和个体理性的。为了验证这些属性的行业，我们首先正式定义这些概念的定理证明，然后制定了许多重要的结果匹配的需求和供应。最后，我们使用这个框架来验证两类重要的双边拍卖机制的性质。本文中给出的所有定义和结果都在Coq证明助手中完全形式化，而不需要添加任何额外的公理。
2020-07-18 cs.DS cs.GT cs.LO
QED at Large: A Survey of Engineering of Formally Verified Software
开发程序正确性的形式化证明可以增加实际和感知的可靠性，并有助于更好地理解程序规范及其基本假设。支持这种发展的工具已有40多年的历史，但直到最近才得到广泛的实际使用。基于机器检查的形式化证明的构建的项目现在达到了前所未有的规模，可以与大型软件项目相媲美，这导致了证明开发和维护的新挑战。尽管其日益重要，证明工程领域很少考虑自己的权利;相关的理论，技术和工具跨越许多领域和场所。这篇文献综述对程序正确性的证明工程有了全面的了解，包括在实践中的影响、基础、证明自动化、证明组织和实际证明开发。
2020-03-13 cs.LO cs.PL
Formally Verified Animation for RoboChart using Interaction Trees
本文使用交互树为RoboChart提供操作语义，在Isabelle中实现并生成可执行动画，通过化学探测器和巡逻机器人案例验证了动画场景是CSP指称语义的迹细化，确保了方法的正确性。
2023-09-13 cs.LO
Formally Verified Liveness with Multiparty Session Types in Rocq
University of Edinburgh（爱丁堡大学）；University of Oxford（牛津大学）；School of Computer Science and Engineering, University of New South Wales（新南威尔士大学计算机科学与工程学）
本文在Rocq证明助手中首次机械化证明了同步多方会话类型的活性，利用共归纳树和子类型关系建立局部类型与全局类型的操作对应，从而保证会话的安全性和活性。
2026-05-22 cs.LO
Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces
本文提出一种基于张量语义的LTLf形式化方法，在Isabelle/HOL中验证正确性，并集成到神经符号学习中，通过可微损失函数实现约束训练，提供严谨且高效的框架。
2025-01-23 cs.AI cs.LG cs.LO
Creating a Formally Verified Neural Network for Autonomous Navigation: An Experience Report
Maynooth University（梅努斯大学）
本文通过案例研究探索了在自定义数据集上结合可微逻辑训练自主导航神经网络，使其通过设计满足安全属性，并总结了选择与使用神经网络验证器的经验。
2024-11-21 cs.CV cs.LG cs.LO
VEL: A Formally Verified Reasoner for OWL2 EL Profile
Kansas State University（堪萨斯州立大学）
针对OWL推理器可靠性不足的问题，研究者开发了经形式化验证的EL++推理器VEL，基于Coq证明助手实现算法提取并修正了原算法的完备性缺陷，为高风险场景下的推理正确性提供了保障。
2024-12-11 cs.AI cs.LO cs.PL
Logical Relations for Formally Verified Authenticated Data Structures
本文提出基于新型关系分离逻辑的形式化证明方法，为可自动生成认证数据结构的库验证安全性与正确性，证明了库优化的正确性及手写实现与自动生成代码的可靠链接，结果已在Coq中通过Iris框架机械化验证。
2025-01-18 cs.LO cs.PL
A Formally Verified Procedure for Width Inference in FIRRTL
Key Laboratory of System Software (Chinese Academy of Sciences)（系统软件重点实验室）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；University of Chinese Academy of Sciences（中国科学院大学）；Nanjing Institute of Software Technology（南京软件工程研究所）；Birkbeck, University of London（伦敦大学伯贝克学院）
本文提出了一种正式验证的FIRRTL宽度推断过程，通过定理证明器Rocq实现，并在OCaml中提取出首个正式验证的InferWidths阶段实现。
2026-01-19 cs.LO cs.PL
A Formally Verified HOL4 Algebra for Event Trees
事件树（ET）分析作为一种前向演绎安全分析技术，在关键系统设计阶段被广泛用于决策。ET是表示系统中所有可能的操作状态和外部事件的示意图，以便这些可能的场景之一可能发生。在这份报告中，我们建议使用HOL 4定理证明的形式化建模和步骤分析的ET图。为此，我们在高阶逻辑中开发了一种基于通用列表数据类型的ET图的形式化，该数据类型可以：（i）构建任意级别的ET图;（ii）减少不相关的ET分支;（iii）划分ET路径;以及（iv）基于某些事件的发生进行概率分析。为了说明的目的，我们进行正式的ET逐步分析的电网，并确定其系统平均中断频率指数（SAIFI），这是一个重要的指标，系统的可靠性。
2020-04-29 cs.LO cs.SY eess.SY
Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
Beneficial AI Foundation（有益人工智能基金会）
本文引入最大形式化验证基准FVAPPS（含4715样本），将APPS的Python单元测试泛化为Lean 4未证明定理，测试显示Sonnet和Gemini证明正确率为30%和18%，挑战相关社区解决编程问题及正确性规范。
2025-02-08 cs.AI cs.LG cs.LO
Formally Verifying a Transformation from MLTL Formulas to Regular Expressions
本文在 Isabelle/HOL 中形式化验证了将 MLTL 公式转换为等价正则表达式的 WEST 算法的正确性，并通过代码导出实验验证了现有 WEST 工具。
2025-01-29 cs.LO
From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware
Ledger；Telecom Paris（巴黎电信学院）；Ledger Donjon
本文提出Encore!虚拟机，通过延续传递风格运行Rocq提取的Scheme代码，实现微控制器固件的形式化验证，并利用大语言模型辅助策略合成自动证明固件正确性。
2026-09-22 cs.LO cs.PL cs.SE
Are Users More Willing to Use Formally Verified Password Managers?
本研究通过两项实验（15人形成性研究及200人定量研究）探究用户对形式化验证密码管理器的态度，发现用户视其为可取，并提出三项沟通改进建议。
2025-09-07 cs.CR cs.HC cs.LO
Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline
Ascendr, Inc.（Ascendr公司）
本文提出一种混合AI与Lean 4的正式验证框架，用于专利分析。通过依赖类型理论，实现了专利自由实施、权利主张敏感性、交叉权利主张一致性等五种知识产权应用场景的正式化验证，利用Lean 4进行机器验证，确保计算的数学正确性。
2026-04-20 cs.AI cs.LO cs.PL
Phoenix: A Formally Verified Regenerating Vault
获得加密货币用户私钥访问权限的攻击者可以代替她执行任何操作。由于大多数加密货币的分散性，没有实体可以恢复这些操作。这是去中心化系统面临的一个核心挑战，许多引人注目的抢劫案就说明了这一点。保险库合同通过引入人为的操作延迟来降低这种风险，允许合同所有者在延迟期间流产。然而，钥匙被盗仍然使金库无法使用，并使资金处于危险之中。我们介绍凤凰，一种新颖的合同体系结构，允许用户恢复其安全属性后，密钥丢失。Phoenix利用用户将密钥存储在容易获得但不太安全的存储（第二层）以及更安全但更难访问的存储（第一层）中的能力。与以前的解决方案不同，用户可以在第二层密钥被盗后恢复Phoenix安全性，并且即使在任何一层中丢失密钥也不会丢失资金。Phoenix还引入了一种机制，以减少攻击者在第一层妥协的情况下可能造成的损害。我们正式指定了Phoenix所需的行为，并提供了Phoenix作为以太坊合约的原型实现。由于这样的实现是高度敏感的，容易受到微妙的错误，我们应用形式化验证工具来证明特定的代码属性和识别故障。我们强调了该工具识别的一个错误，该错误可能被攻击者利用来危害Phoenix。在修复缺陷后，该工具证明了底层可执行代码的正确性。
2021-06-02 cs.CR cs.LO
A Verified Algorithm Enumerating Event Structures
事件结构是对事件之间的因果关系、冲突和并发等概念进行数学抽象建模。虽然许多其他数学结构，包括群、拓扑空间、环，有大量的算法和公式来生成、枚举和计数其成员的特定集合，但没有已知的算法或公式来生成或计数有限事件集合上的所有可能的事件结构。我们提出了一个算法来生成这样一个家庭，以及使用Isabelle/HOL验证的功能实现。作为副产品，我们得到了所有可能的前序和偏序的验证枚举。虽然计数前序和偏序的整数序列已经在OEIS（On-line Encyclopedia of Sequences）中列出，但计数事件结构的整数序列还没有。因此，我们使用我们的算法提交了一份正式验证的补充文件，该文件已成功通过审查，现在是OEIS的一部分。
2017-05-20 cs.LO
LeanBET: Formally-verified surface area calculations in Lean
University of Maryland, Baltimore County（马里兰大学巴尔的摩分校）
本文在Lean4中实现并验证了BET方法的完整流程，包括窗口枚举、单调性检查、膝点选择和线性回归，证明了算法的正确性并验证了与BETSI参考方法的一致性。
2026-05-15 cs.LO cs.MS physics.chem-ph
Let it Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow
Carnegie Mellon University（卡内基梅隆大学）；University of Maryland, College Park（马里兰大学帕克分校）
该研究提出首个异步数据流编译器的形式化验证框架Wavelet，通过带围栏的能力类型系统等技术，验证编译器核心 passes 并证明相关属性，编译的数据流图规模与未经验证编译器相当。
2026-08-07 cs.LO cs.PL
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
The Trusted Computing Base of the CompCert Verified Compiler
CompCert是第一个现实的正式验证编译器：它提供了一个机器检查的数学证明，证明它生成的代码与源代码匹配。然而，这种做法可能存在漏洞。我们全面分析了CompCert的错误可能导致生成错误代码的方面。可能的问题包括从源语言和目标语言的建模到用于从编译器内部调用外部算法的某些技术。
2022-10-10 cs.LO cs.PL
Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
UC Berkeley（伯克利大学）；Google（谷歌）；UC Santa Cruz（圣克鲁兹大学）
提出归纳演绎合成（IDS）方法，通过联合增量合成实现与证明，并利用失败尝试学习，使AI在分布式系统规范上实现100%验证成功率，成本和时间远低于专家和现有AI代理。
2026-05-22 cs.AI cs.DC cs.LO
Vero: Can AI Agents Build Formally Verified Software Repositories?
University of Chicago（芝加哥大学）；California Institute of Technology（加州理工学院）；Stanford University（斯坦福大学）；UC Berkeley（加州大学伯克利分校）；Amazon Web Services（亚马逊云计算服务）；Apodex
研究推出首个仓库级验证软件综合基准Vero，含43个多模块实例，评估发现前沿智能体仅解决27个实例，为相关研究提供测试平台。
2026-08-14 cs.AI cs.LG cs.LO
A Verified Decision Procedure for Orders in Isabelle/HOL
我们提出了第一个验证执行的决定程序的量化自由理论的部分和线性订单。我们正式的程序在伊莎贝尔/HOL，并提供了一个规范，可执行使用伊莎贝尔的代码生成器。该程序已经是Isabelle开发版本的一部分，作为加密器的子程序。
2021-07-02 cs.LO
Formally Verified Next-Generation Airborne Collision Avoidance Games in ACAS X
飞机防撞算法的设计是一个微妙但重要的挑战，值得证明安全保证的需要。考虑到入侵飞机决策、本机驾驶员反应和飞机连续运动动力学的微妙性之间的相互作用的不可预测性，获得这样的保证是不平凡的。现有的防撞系统，如TCAS和下一代机载防撞系统ACAS X，已经被分析为假设对入侵者的飞行机动有严格的限制，限制了它们在入侵者可能改变航向的真实场景中的安全保证。这项工作需要一个概念上的显着和实际相关的偏离现有的ACAS X模型，将它们推广到混合游戏与一流的代表性的所有权和入侵者的决定来自两个独立的球员，使显着先进的预测能力。通过证明微分博弈逻辑中的对抗性ACAS X的获胜策略的存在性，建立了本机和入侵者飞机的丰富遭遇的碰撞自由，沿着具有不断变化的垂直/水平速度的飞行路径的微分方程具有独立的决策。我们提出了三种类型的模型的复杂性不断增加：单咨询无限时间模型，有界时间模型，无限时间，多咨询模型。在每一类模型中，我们确定象征性的条件，并证明，然后总是有一个可能的本机机动，将防止两架飞机之间的碰撞。
2022-03-01 cs.GT cs.LO cs.SY
A Formally Specified Type System and Operational Semantics for Higher-Order Procedural Variables
我们使用Ott和Isabelle/HOL证明助手正式地定义了LOOPw的类型系统和操作语义。此外，类型系统和语义的LOOPw已经测试使用Isabelle/HOL程序提取设施归纳定义的关系。特别是，计算Ackermann函数的程序会进行类型检查并按预期运行。LOOPw的主要区别（除了选择类似于Ada的具体语法之外）来自对参数传递的处理。实际上，由于Ott目前并不完全支持alpha转换，因此我们使用显式别名来重新表述操作语义，以便实现输出参数传递模式。
2009-10-06 cs.LO
Aligning HOL-Light and Rocq libraries formally
INRIA（法国国家信息与自动化研究所）；ENS Paris-Saclay（巴黎萨克雷高等师范学院）；CNRS（法国国家科学研究中心）
本文报告了将 HOL-Light 定理形式化翻译至 Rocq 的工作，开发自动化策略替换定义，并引入实数、R^n 空间及极限等新形式化内容。
2026-09-22 cs.LO
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem
计算机代数和数值分析中的许多问题都可以归结为计算或近似计算一个区间内多项式的实根。现有的主要证明助手中的已验证根计数过程主要基于经典的Sturm定理，该定理仅计数不同的根。在本文中，我们加强了根计数能力在Isabelle/HOL的第一次正式证明布丹-傅立叶定理。随后，基于笛卡尔的符号规则和泰勒移位，我们已经提供了一个验证过程，有效地过近似的实根的数量在一个区间内，计数重。为了准确地计算多重根，我们扩展了我们以前的Sturm定理的形式化。最后，我们结合验证组件在上述发展，以改善我们以前的认证复根计数程序的基础上柯西指数。我们相信这些经过验证的例程对于认证程序和构建策略至关重要。
2018-11-27 cs.LO
Pursuit of Truth and Beauty in Lean 4: Formally Verified Theory of Grammars, Optimization, Matroids
Institute of Science and Technology Austria（奥地利科学技术学院）
本文通过形式化验证探讨数学中的语法理论、优化与Matroid理论，旨在创建可理解、可信、有用且优雅的代码，强调定义的可读性和可信度，而非易于操作的定义。
2026-03-25 cs.LO math.HO
Formally Verifying the Safety of Pipelined Moonshot Consensus Protocol
本文使用IVy对Supra的Pipelined Moonshot共识协议进行形式化建模与验证，证明在拜占庭验证者少于三分之一时协议无分叉且能防止双花攻击。
2024-03-25 cs.LO
On the Formalization of the Heat Conduction Problem in HOL
偏微分方程（PDE）被广泛地用于物理现象的建模和许多工程和物理系统的动力学行为的分析。热方程是最著名的偏微分方程之一，它描述了物体内部的温度分布和热扩散。由于这些方程在各种安全关键应用中的广泛应用，例如热保护系统，热传递的形式分析是至关重要的。在本文中，我们提出使用高阶逻辑（HOL）的定理证明形式化分析热传导问题的直角坐标系。特别是，我们使用HOL Light定理证明器的多变量微积分理论，将传热正式建模为矩形板的一维热方程。这就需要形式化的热算子和形式化验证的各种属性，如线性和缩放。此外，我们使用分离变量法正式验证的解决方案的偏微分方程，它允许模拟在各种初始和边界条件下，使用HOL光在板的传热。
2022-08-13 cs.LO
CSLib: The Lean Computer Science Library
Amazon（亚马逊）；Stanford University（斯坦福大学）；Google DeepMind（谷歌DeepMind）；The University of Texas at Austin（德克萨斯大学奥斯汀分校）；FORM, University of Southern Denmark（南丹麦大学FORM）；Lean FRO；Atlas Computing（阿特拉斯计算）；Getulio Vargas Foundation（热图利奥·瓦加斯基金会）；Institute for Theoretical Studies, ETH Zürich（苏黎世联邦理工学院理论研究所）
CSLib是一个旨在提升Lean在计算机科学领域应用的开源框架，通过增强形式验证能力促进教育与研究。
2026-02-04 cs.LO cs.PL
A Verified Implementation of B+-Trees in Isabelle/HOL
在本文中，我们提出了无处不在的B+树数据结构的交互式定理证明器Isabelle/HOL的强制性实现的验证。该实现支持成员资格测试，插入和范围查询与有效的二进制搜索节点内导航。命令式实现的验证分为两个步骤：一个抽象的集合接口被细化为一个可执行的，但效率低下的纯功能的实现，这是进一步细化为有效的命令式实现。
2022-08-18 cs.DS cs.LO
Formale Entwicklung einer Steuerung für eine Fertigungszelle mit SYSYFOS
采用Manna和Waldinger的综合方法，开发了一种正式指定和验证的生产单元控制电路。通过建立适当的形式语言层，可以实现对非形式化描述的需求规格说明。我们证明了演绎合成的范式可以应用于开发完整的验证系统，包括硬件和机械。我们定义了两个特定于领域的逻辑运算符，它们在规范和证明中对频繁模式进行了模式化，从而允许更简洁和更有表现力的呈现。在Burghardt（1995）中，可以找到这篇论文的英文简短版本，没有附录。
2014-04-04 cs.LO cs.SE
Verified Probabilistic Policies for Deep Reinforcement Learning
University of Birmingham（伯明翰大学）
深度强化学习是一种越来越流行的技术，用于合成策略以控制代理与其环境的交互。人们对正式验证这些策略是否正确并安全执行的兴趣也越来越大。在这一领域取得的进展是建立在现有工作的基础上，对深层神经网络和连续状态动力系统进行验证。在本文中，我们解决了验证深度强化学习的概率策略的问题，例如，用于解决对抗性环境，打破对称性和管理权衡。我们提出了一个抽象的方法，基于区间马尔可夫决策过程，产生概率保证政策的执行，目前的技术来建立和解决这些模型，使用抽象的解释，混合整数线性规划，基于熵的细化和概率模型检验。我们实现我们的方法，并说明其有效性的选择强化学习基准。
2022-06-01 cs.AI cs.LG cs.LO
Formal Verification of the Sumcheck Protocol
本文使用 Isabelle/HOL 对 sumcheck 协议进行形式化验证，通过模块化方法建立其可靠性和完备性，并证明公理适用于多元多项式，为基于该协议的密码系统提供安全性保障。
2024-02-08 cs.CR cs.LO
GOL in GOL in HOL: Verified Circuits in Conway's Game of Life
本文在HOL4定理证明器中形式化验证了一个通过逻辑电路在康威生命游戏（GOL）中实现GOL的编译器，该编译器能将初始GOL状态转换为可由现成模拟器运行的巨细胞版本，相关技术也适用于其他细胞自动机及硬件验证。
2025-03-31 cs.FL cs.LO cs.SC
