Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL
仿真和形式化验证是基于模型的高可靠性系统开发的重要补充技术。为了支持一致的结果，有必要为这两个活动提供统一的语义和自动化。在本文中，我们应用Isabelle/HOL中的交互树产生一个验证和仿真框架的状态丰富的过程语言。我们开发的核心理论和验证技术的交互树，使用它们给CSP和马戏团的语言的语义，并正式连接我们的新语义与故障分歧的语义模型。我们还展示了如何伊莎贝尔代码生成器可以用来生成验证可执行的模拟反应和并发程序。
2021-05-11 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
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
Logical Relations for Formally Verified Authenticated Data Structures
本文提出基于新型关系分离逻辑的形式化证明方法，为可自动生成认证数据结构的库验证安全性与正确性，证明了库优化的正确性及手写实现与自动生成代码的可靠链接，结果已在Coq中通过Iris框架机械化验证。
2025-01-18 cs.LO cs.PL
A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
本研究提出一种经形式化验证的MDP区间迭代浮点实现，通过Isabelle/HOL完成从抽象语义到LLVM代码的全链路正确性证明，扩展精化框架支持浮点推理，实验表明其性能与前沿工具相当且具备形式化正确性保证。
2025-10-06 cs.LO
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 proof of the Central Limit Theorem
我们描述了一个证明的中心极限定理，已正式核实的伊莎贝尔证明助手。我们的形式化的基础上，并扩展伊莎贝尔的图书馆分析和测量理论的概率。该定理的证明使用特征函数，这是一种傅立叶变换，以证明，在适当的假设下，随机变量的总和弱收敛到标准正态分布。我们还讨论了支持正式化的库和基础设施，并反思了我们从这一努力中吸取的一些教训。
2017-02-01 cs.LO cs.MS math.PR
Duality theory in linear optimization and its extensions -- formally verified
Institute of Science and Technology Austria（奥地利科学技术研究所）
本文通过形式化证明，扩展了Farkas定理至线性有序域，并探讨了允许系数取无限值的对偶理论扩展。
2026-03-06 cs.LO math.OC
A Formally Verified HOL Algebra for Dynamic Reliability Block Diagrams
为了克服传统可靠性框图无法捕捉冗余元件等建模缺陷，引入了动态可靠性框图（DRBDs）。然而，到目前为止，还没有一个代数框架，允许进行分析的一个给定的DRBD的基础上，其结构功能，并能够验证其可靠性使用高阶逻辑（HOL）定理证明。在这项工作中，我们提出了一个新的代数正式表示的结构功能和可靠性的DRBD与备用构造的基础上的基本系统块和新引入的DRBD运营商。我们提出了几个简化属性，允许减少给定DRBD的结构。我们提供了HOL形式化的建议代数，并正式验证其相应的属性使用HOL4定理证明。这包括以可扩展的方式正式验证备用构造、串联、并联和更深层次结构的通用可靠性表达式，从而允许验证复杂系统的可靠性。最后，我们证明了这个代数的适用性，正式分析终端可靠性分析的洗牌交换网络在HOL4。
2019-08-06 cs.LO
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
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
A Formally Verified Lightning Network
本文利用 Why3 平台对闪电网络进行形式化验证，首次提供机器可检查的证明，证明其在所有场景下均能保护诚实用户资金安全。
2025-03-10 cs.CR 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
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
Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified
本文在Lean 4中形式化验证了Seymour定理的正则拟阵组合方向，开发了相关矩阵与拟阵库，适用于有限秩且底集可能无限的情形。
2025-09-24 cs.LO math.CO
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
Formally Verified Trades in Financial Markets
我们介绍了一个分析金融市场交易的正式框架。如今，所有大型交易所都使用计算机算法来匹配买入和卖出请求，这些算法必须遵守某些监管准则。例如，市场监管机构强制要求交易所产生的匹配应该是公平的、统一的和个体理性的。为了验证这些属性的行业，我们首先正式定义这些概念的定理证明，然后制定了许多重要的结果匹配的需求和供应。最后，我们使用这个框架来验证两类重要的双边拍卖机制的性质。本文中给出的所有定义和结果都在Coq证明助手中完全形式化，而不需要添加任何额外的公理。
2020-07-18 cs.DS cs.GT cs.LO
The Trusted Computing Base of the CompCert Verified Compiler
CompCert是第一个现实的正式验证编译器：它提供了一个机器检查的数学证明，证明它生成的代码与源代码匹配。然而，这种做法可能存在漏洞。我们全面分析了CompCert的错误可能导致生成错误代码的方面。可能的问题包括从源语言和目标语言的建模到用于从编译器内部调用外部算法的某些技术。
2022-10-10 cs.LO cs.PL
Certified Knowledge Compilation with Application to Formally Verified Model Counting
针对知识编译输出缺乏正确性保证的问题，提出分区操作图（POGs）及CPOG证明框架，并开发基于D4的生成与验证工具链及Lean 4形式化验证的模型计数器，构成首个形式化验证的模型计数工具链。
2025-01-22 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 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
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
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
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
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
Are Users More Willing to Use Formally Verified Password Managers?
本研究通过两项实验（15人形成性研究及200人定量研究）探究用户对形式化验证密码管理器的态度，发现用户视其为可取，并提出三项沟通改进建议。
2025-09-07 cs.CR cs.HC cs.LO
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
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
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 Revised and Verified Proof of the Scalable Commutativity Rule
本文解释了可扩展交换性规则（SCR）的公开证明中的一个缺陷，在Coq证明助手中给出了SCR的修改和正式验证的证明，并讨论了我们证明SCR的经验中提出的见解和开放性问题。
2018-09-23 cs.DC cs.LO
Phoenix: A Formally Verified Regenerating Vault
获得加密货币用户私钥访问权限的攻击者可以代替她执行任何操作。由于大多数加密货币的分散性，没有实体可以恢复这些操作。这是去中心化系统面临的一个核心挑战，许多引人注目的抢劫案就说明了这一点。保险库合同通过引入人为的操作延迟来降低这种风险，允许合同所有者在延迟期间流产。然而，钥匙被盗仍然使金库无法使用，并使资金处于危险之中。我们介绍凤凰，一种新颖的合同体系结构，允许用户恢复其安全属性后，密钥丢失。Phoenix利用用户将密钥存储在容易获得但不太安全的存储（第二层）以及更安全但更难访问的存储（第一层）中的能力。与以前的解决方案不同，用户可以在第二层密钥被盗后恢复Phoenix安全性，并且即使在任何一层中丢失密钥也不会丢失资金。Phoenix还引入了一种机制，以减少攻击者在第一层妥协的情况下可能造成的损害。我们正式指定了Phoenix所需的行为，并提供了Phoenix作为以太坊合约的原型实现。由于这样的实现是高度敏感的，容易受到微妙的错误，我们应用形式化验证工具来证明特定的代码属性和识别故障。我们强调了该工具识别的一个错误，该错误可能被攻击者利用来危害Phoenix。在修复缺陷后，该工具证明了底层可执行代码的正确性。
2021-06-02 cs.CR 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
Verified Real Number Calculations: A Library for Interval Arithmetic
在机械证明中，初等函数的实数计算是非常困难的。在本文中，我们将展示如何在一个定理证明器或证明助手中以一种方便、高度自动化和交互式的方式进行这些计算。首先，我们正式建立了初等函数的上界和下界。然后，基于这些界限，我们开发了一个合理的区间算术实数计算发生在代数设置。为了减少区间算术的依赖效应，我们结合了两种技术：区间分裂和泰勒级数展开。这种务实的方法已经开发，并正式验证，在定理证明。正式的开发还包括一组可定制的策略，以自动化涉及实数显式计算的证明。我们的最终目标是提供有保证的数值性质的证明与最小的人类定理证明者的相互作用。
2007-08-28 cs.LO cs.MS
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
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
Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition
硬件加速器（HA）是快速和节能计算系统的基本构建模块。加速器快速错误检测（A-QED）是一种新的形式化技术，它使用有界模型检验进行HA的预硅验证。A-QED检查HA的自一致性，即，在一个操作序列中，相同的输入是否总是产生相同的输出。在适度的假设下，A-QED既合理又完整。然而，众所周知，大的设计尺寸显著地限制了包括A-QED的形式化验证的可扩展性。我们克服了这个可扩展性的挑战，通过一个新的A-QED分解技术，称为A-QED与分解（A-QED $^2$）。A-QED $^2$系统地将HA分解为更小的功能子模块，称为子加速器，然后使用A-QED独立验证。我们证明完整的A-QED $^2$，特别是，如果在验证下的完整HA包含一个错误，那么A-QED $^2$确保检测到该错误在A-QED验证相应的子加速器。对100多个不同版本的具有数百万逻辑门的HA的结果证明了A-QED $^2$的有效性和实用性。
2021-08-17 cs.LO
Formally Verifying a Transformation from MLTL Formulas to Regular Expressions
本文在 Isabelle/HOL 中形式化验证了将 MLTL 公式转换为等价正则表达式的 WEST 算法的正确性，并通过代码导出实验验证了现有 WEST 工具。
2025-01-29 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
Proving soundness of combinatorial Vickrey auctions and generating verified executable code
使用机械化的推理，我们证明了组合Vickrey拍卖是健全的规定，他们将一个独特的结果（分配和转让）的任何有效的输入（出价）。这样做之后，我们从正式定义的拍卖中自动生成经过验证的可执行代码。这消除了在实现拍卖设计中的错误来源。我们打算使用正式的方法来验证新的拍卖设计。在这里，我们的贡献是介绍和展示使用正式的方法进行拍卖验证在熟悉的设置一个著名的拍卖。
2013-09-02 cs.CE cs.GT 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
Fundamental Limits in Formal Verification of Message-Passing Neural Networks
University of Kassel（卡塞尔大学）
输出可达性和对抗鲁棒性是神经网络最相关的安全属性之一。我们表明，在消息传递神经网络（MPNN）的背景下，一个常见的图神经网络（GNN）模型，形式化验证是不可能的。特别是，我们表明，输出可达的图分类MPNN，工作在图的无界大小，非平凡程度和充分表达节点标签，不能正式验证：有没有算法，正确回答（是或否），给定一个MPNN，是否存在一些有效的输入MPNN，使相应的输出满足给定的规格。然而，我们也表明，输出的可达性和对抗性的鲁棒性节点分类MPNN可以正式验证时，输入图的程度的限制是先验的。我们讨论了这些结果的影响，为了获得一个完整的图片的原则可能性，正式验证GNN，根据所涉及的GNN模型和输入输出规格的表现力。
2022-10-04 cs.LG 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
Formally Certified Approximate Model Counting
National University of Singapore（新加坡国立大学）；Chalmers University of Technology（查尔姆斯理工大学）；University of Toronto（多伦多大学）
该研究提出首个近似模型计数认证框架，结合Isabelle/HOL静态形式化证明与动态证明证书验证，在低开销下实现对ApproxMC输出近似质量的形式化保证。
2024-06-19 cs.AI cs.LO
The Design and Regulation of Exchanges: A Formal Approach
我们使用正式的方法来指定，设计和监控连续的双向拍卖，这被广泛用于匹配买家和卖家在外汇，股票和商品交易所。我们确定了三个自然属性，这样的拍卖，并正式证明，这些属性完全决定的投入产出关系。然后，我们正式验证，一个自然的算法满足这些属性。所有的定义、定理和证明都在一个交互式定理证明器中正式化。我们提取我们的算法的验证程序来构建一个自动检查器，如果交易所生成的交易违反了任何自然属性，该检查器可以保证检测到交易日志中的错误。
2022-10-11 cs.LO q-fin.TR
Industrial-Strength Formally Certified SAT Solving
University of Southampton（南安普顿大学）；University College Dublin（都柏林大学学院）
布尔可满足性（SAT）求解器现在经常用于大型工业问题的验证。然而，它们在安全关键领域（如铁路、航空电子和汽车行业）的应用需要某种形式的结果保证，因为求解器可能（有时确实）有错误。不幸的是，现代的，高度优化的SAT求解器的复杂性，使不切实际的直接形式证明其正确性的发展。本文提出了一种替代方法，其中一个不可信的，工业强度，SAT求解器插入到一个可信的，正式认证，SAT证明检查提供工业强度认证的SAT解决方案。我们的方法的主要新颖性和特点是：（一）检查器是自动提取的正式开发，（二），组合系统可以作为一个独立的可执行程序独立于任何支持定理证明，及（iii）检查器证明任何SAT求解器尊重商定的格式可满足性和不可满足性索赔。该系统的核心是一个经过认证的检查器，用于检查在Coq中正式设计和验证的不可满足性声明。我们提出了它的形式化设计和大纲的正确性证明。实际的独立检查器是从Coq开发中自动提取的。一个有代表性的一组工业基准从SAT竞赛的认证检查器的评估表明，虽然它是慢于未经认证的SAT检查器，它是显着快于认证的检查器上实现的交互式定理证明。
2009-12-17 cs.AI cs.LO
Formale Entwicklung einer Steuerung für eine Fertigungszelle mit SYSYFOS
采用Manna和Waldinger的综合方法，开发了一种正式指定和验证的生产单元控制电路。通过建立适当的形式语言层，可以实现对非形式化描述的需求规格说明。我们证明了演绎合成的范式可以应用于开发完整的验证系统，包括硬件和机械。我们定义了两个特定于领域的逻辑运算符，它们在规范和证明中对频繁模式进行了模式化，从而允许更简洁和更有表现力的呈现。在Burghardt（1995）中，可以找到这篇论文的英文简短版本，没有附录。
2014-04-04 cs.LO cs.SE
