Encapsulating Formal Methods within Domain Specific Languages: A Solution for Verifying Railway Scheme Plans
形式化方法的发展和应用是计算机科学领域一个长期的研究课题。仍然存在的一个特殊挑战是将正式方法纳入工业实践。本文介绍了一种方法，用于开发领域特定的语言建模和验证，以帮助在工业中的正式方法的吸收。它说明了这种方法在铁路领域的成功应用。所提出的方法解决问题，围绕忠实的建模，可扩展性的验证和访问的建模和验证过程中的从业者在域。
2014-03-23 cs.LO cs.SE
A Summary of Formal Specification and Verification of Autonomous Robotic Systems
自主机器人系统是复杂的，混合的，通常是安全关键的;这使得它们的形式化规范和验证具有独特的挑战性。虽然通常使用，但单独的测试和模拟不足以确保自主机器人的正确性，或为自主机器人的认证提供足够的证据。自主机器人的形式化方法在文献中得到了一些关注，但没有资源提供当前的概述。这篇简短的论文总结了Luckcuck 2019的贡献，该论文调查了自主机器人正式规范和验证的最新技术。
2019-11-25 cs.SE
Integrating Formal Verification and Simulation-based Assertion Checking in a Corroborative V&V Process
自动驾驶汽车（Automated Vehicles，简称AV）在交通领域正迅速成熟。然而，AV设计问题的复杂性是这样的，没有一种技术足以提供关键属性，如安全性，可靠性或可信度的充分验证。在这篇愿景论文中，提出了一种空间交通逻辑和基于代理的验证方法与验证方法相结合的方法，该方法使用断言检查模拟。我们概述了如何将各自的方法集成到一个名为“确证验证与确认”（V&V）的方法框架中。确证验证与确认框架为AV确定了三个不同的验证和确认级别（形式化验证、基于模拟的测试、真实世界实验）并指定了这些级别之间的联系和证据。我们定义了必须在过程、系统模型和需求模型之间建立的正式关系的规范，这些关系是来自正式设计验证和基于模拟的测试的证据，以相互证实并增强验证和确认的保证信心。
2022-08-10 cs.SE
A survey on formal specification and verification of separation kernels
分离内核是安全和安全关键系统的基础软件，它为托管应用程序提供空间和时间分离以及分区之间的受控信息流。分离核在关键领域的应用要求通过形式化验证来验证分离核的正确性。据我们所知，没有关于这一主题的调查文件。本文综述了分离核的形式化描述和验证。本文首先介绍了分离核的概念和背景，并对不同分离核进行了比较。然后，我们调查了自2000年以来关于这个主题的最新技术。最后，通过详细的比较和讨论，对研究工作进行了总结.
2016-07-10 cs.SE
Generating Logical Specifications from Requirements Models for Deduction-based Formal Verification
工作涉及自动生成的逻辑规格的需求模型。以这种方式获得的逻辑规范可以使用演绎推理进行形式化验证。形式化验证关注模型行为的正确性。需求工程的可靠性对于软件开发过程的所有阶段都是必不可少的。演绎推理是一种重要的形式化方法。然而，逻辑规范，被认为是一组时序逻辑公式，很难指定手动经验不足的用户，这一事实可以被视为一个重大障碍，实际使用的演绎为基础的验证工具。提出了一种利用UML图建立需求模型的方法，包括逻辑规格说明。将活动图组织到预定义的工作流模式中可以自动提取逻辑规范。所提出的方法的关键方面是集成的需求工程阶段和逻辑规格的自动生成。提出了一种基于演绎的验证系统。推理过程可以基于语义表方法。提供了一个简单的需求获取和验证的示例。
2014-02-09 cs.SE
A Methodology for Developing a Verifiable Aircraft Engine Controller from Formal Requirements
验证复杂的安全关键系统是一项重大挑战。手动测试和模拟经常使用，但只能探索系统可达状态的子集。形式化方法是一种基于知识的软件规格说明和开发技术，它可以提供系统状态空间上的属性证明和穷举检查。在本文中，我们提出了一个正式的需求驱动的方法，适用于我们的工业合作伙伴提供的飞机发动机控制器的模型。我们的方法开始正式化的控制器的自然语言的要求，使用（预先存在的）正式的需求获取工具（FRET），迭代，与我们的行业合作伙伴协商。一旦形式化，FRET可以自动转换的要求，使他们的验证旁边的Simulink模型的飞机发动机控制器;的要求也可以指导形式化验证使用其他方法。在我们的方法中，这两个并行流寻求结合正式的需求引出，经典的验证方法和运行时验证的结果，以支持在Simulink中建模的航空航天系统的验证，从需求阶段到执行。我们的方法利用正式方法的力量，补充现有的验证技术，并支持整个验证过程中的需求的可追溯性。这种方法通过确保预先正式化要求并在开发过程中可用，简化了开发可验证飞机发动机控制器的过程。在本文中，我们给出了一个概述（FRET），描述我们的方法和工作的形式化和验证的要求，并概述了未来的工作，使用我们的方法。
2021-10-18 cs.SE
Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)
本文提出通过将 Stipula 法律合同翻译为带 JML 规范的 Java 代码，并利用 KeY 工具自动验证其部分和完全正确性，证明了通用演绎验证工具在翻译方法中的有效性。
2025-09-26 cs.SE
Towards A Broader Acceptance Of Formal Verification Tools: The Role Of Education
形式化方法虽然具有优势，但在软件开发实践中面临着广泛接受和采用的挑战。主要原因是假设的复杂性。学术界可以通过一个深思熟虑的教学和实践计划来解决这个问题。本文中详细介绍的用户研究正在检查AutoProof工具，其动机是识别形式化方法的复杂性。参与者（计算机科学硕士课程的学生）的表现和反馈的经验与正式的方法帮助我们提取特定的问题领域，影响工具的可用性。研究结果推断，随着验证工具功能的改进，教学计划必须修改，以包括先决条件的课程，使形式化方法易于学生适应，并促进其在软件开发过程中的使用。
2019-06-04 cs.SE
Towards Formal Verification of a TPM Software Stack
本文基于Frama-C对开源TPM软件栈tpm2-tss开展形式化验证案例研究，针对链表和复杂数据结构带来的挑战提出解决方案，验证了代表性函数的功能性质与无运行时错误，并指出实现完整验证所需的工具改进。
2023-10-27 cs.SE
Bus Protocols: MSC-Based Specifications and Translation into Program of Verification Tool for Formal Verification
消息序列图（MSC）是一种吸引人的可视化形式主义，主要用于系统设计的早期阶段，以捕获系统的需求。然而，如果我们走向一个实现，一个可执行的规范，以某种方式相关的MSC为基础的要求，必须获得。MSC可以有效地用于指定总线协议的方式，其中高级转换系统用于捕获协议的系统组件的控制流，MSC用于描述非原子组件的交互。该规范系统可进行形式化验证。在本文中，我们提出的方式，我们可以指定的总线协议，使用MSC和这些规格说明如何可以转换成程序的验证工具（我们已经使用的符号模型验证器（SMV））使用的形式化验证。在这方面，我们为以下任务作出了贡献。首先，介绍了利用MSC来指定协议的方法。其次，一个翻译器，翻译的规范（描述在文本输入文件）到SMV程序已经建成。最后，我们给出了使用SMV程序对AMBA总线协议进行验证的结果。通过转换过程找到的SMV程序可以用于自动验证任何指定的总线协议的各种属性。
2010-09-26 cs.SE
Formal Specification and Verification of Solidity Contracts with Events
Solidity语言中的事件提供了去中心化应用程序的链上服务与这些服务的用户之间的通信方式。事件通常被用作从用户的角度来看相关的合约执行的抽象。因此，用户必须能够理解所发出事件的含义并信任其有效性。本文提出了一种源代码级的方法，用于Solidity合同的形式化规范和验证，主要关注事件。我们的方法允许根据事件跟踪的链上数据来指定事件，以及定义区块链状态与事件提供的抽象视图之间的对应关系的谓词。该方法是在solc验证，Solidity的模块化验证，我们证明了它的适用性与各种例子。
2020-05-20 cs.LO cs.PL cs.SE
Formal Verification, Engineering and Business Value
如何将模型检验和静态程序分析等自动化验证技术应用于数百万行嵌入式C/C++代码？如何将这种技术包装成软件开发人员和工程师可以使用的方式，他们可能没有形式化验证的背景？以及如何说服企业经理实际支付这样的软件？这项工作解决了其中一些问题。基于我们自己开发和发布Goanna源代码分析器的经验，我们解释了模型检验，静态分析和SMT解决的底层技术，涉及创建工业证明工具的步骤。
2013-01-01 cs.SE
Towards the Formal Specification and Verification of Maple Programs
在本文中，我们提出了我们正在进行的工作和初步结果的形式规范和验证的MiniMaple（一个重要的子集Maple轻微扩展）程序。我们工作的主要目标是在这些程序中找到行为错误。通过静态分析确定其规格。这项任务是更复杂的广泛使用的计算机代数语言，如Maple，因为这些是从根本上不同于经典的语言：它们支持非标准类型的对象，如符号，未评估的表达式和多项式，并需要抽象的计算机代数概念和对象，如环和排序等作为一个出发点，我们已经定义和形式化的语法，语义，类型系统和规约语言的MiniMaple。
2012-07-10 cs.LO cs.MS cs.PL
A User Study for Evaluation of Formal Verification Results and their Explanation at Bosch
该研究针对博世汽车工程师开展调研与实验，发现形式化方法应用存在理解难点，验证了反例解释方法可降低验证结果理解难度，为工业界形式化方法落地提供参考。
2023-04-18 cs.SE
Specification and Verification of Context-dependent Services
当前用于服务的发现、规范和提供的方法忽略了服务契约与服务可以保证其契约的条件之间的关系。此外，它们没有使用正式的方法来指定服务、契约和组合。没有正式的基础，就不可能通过形式化验证来证明服务组合的正确性条件和服务条款中合同义务的履行。我们在本文中纠正这种情况。我们提出了一个正式的定义与上下文相关的合同服务。我们定义了一个组合理论的服务与上下文相关的合同考虑到功能，非功能，法律和上下文信息。最后，我们提出了一个形式化验证方法，将服务组合的形式化规范转换为扩展的时间自动机，可以使用模型检验工具UPPAAL进行验证。
2011-08-11 cs.SE
Requirement analysis, Architectural design and Formal verification of a multi-agent based University Information Management System
提出了一种基于多Agent的高校信息管理系统的分析、设计和形式化验证方法。大学IMS访问信息，创建报告，方便教师和学生。协调器代理管理所有代理之间的协调。它还管理整个系统的数据库连接。建议的IMS是基于BDI代理体系结构，该模型的基础上的信念，愿望和意图的系统。安全性和活性的正确性性质由一阶谓词逻辑指定。
2015-01-06 cs.SE
A Survey of Smart Contract Formal Specification and Verification
智能合约是一种计算机程序，允许用户在区块链平台上自动执行操作。鉴于智能合约在支持包括供应链、金融、法律和医疗服务在内的各行业重要活动方面的重要性，对验证和确认技术的需求非常强烈。然而，绝大多数智能合约缺乏任何形式的规范，这对于确定其正确性至关重要。在本次调查中，我们调查了文献中提出的智能合约的正式模型和规范，并提出了一个系统的概述，以了解共同的趋势。我们还讨论了目前使用的方法，在验证这些属性的规格，并确定差距，希望认识到有前途的方向，为未来的工作。
2021-04-19 cs.SE
A User-Study Protocol for Evaluation of Formal Verification Results and their Explanation
背景：由于特征和功能的数量不断增加，工业中现代安全关键系统的复杂性不断增加。这就需要正式的方法，以信任这样的系统。然而，由于可用性问题，在工业中使用正式方法是有要求的，例如，理解模型检验结果的困难。因此，假设是，以用户友好的方式呈现模型检查器的结果可以促进正式方法在行业中的使用。目的：我们的目标是评估工程师接受的形式化方法，如果理解验证结果的复杂性变得容易。方法：我们进行了两项不同的探索性研究。首先，我们进行了一项在线调查，以探讨在识别不一致的规范和使用正式的方法，从工程师的挑战。其次，我们进行了一组前测和后测实验，以收集工程师使用正式的方法，如果理解验证结果是容易的印象。局限性：本研究的主要局限性是概括性，因为调查集中在一个特定的目标群体，它使用了前实验设计。
2021-08-13 cs.SE
Verification of Design Decisions in Communication Protocol by Evaluation of Temporal Logic Formulas
在通信协议的设计过程中，许多设计决策会影响协议的行为及其正确性。协议的形式化规范和验证可以证明其正确性。本文给出了一个利用CSM自动机的形式规格说明和时序逻辑验证设计决策的实例。
2017-10-25 cs.SE
Requirements, Formal Verification and Model transformations of an Agent-based System: A CASE STUDY
在多智能体系统的软件规格工程中，最具挑战性的任务之一是确保正确性。由于这些系统具有高并发性，通常具有动态环境，这些系统的形式化规范和验证以及从抽象到具体概念的逐步细化在系统正确性中起着重要作用。我们的目标是正式规范，分析功能以及非功能属性逐步细化从抽象到具体的规范，然后形式化验证这些规范。多智能体系统是一个多进程并行工作的并发系统。我们已经在盖亚多智能体方法与有限状态过程为基础的有限自动机技术，因此，我们已经定义了我们的系统的正式规格，检查的正确性和验证所有可能的流程并发执行这些规格。我们的贡献在于将基于组织抽象的需求规范转换为基于有限自动机的可执行形式化验证规范。我们已经考虑了一个案例研究，我们的多智能体系统，以确保正式的规范和验证。
2015-01-21 cs.MA cs.SE
Formal Verification of Dynamic and Stochastic Behaviors for Automotive Systems
功能和非功能需求的形式化分析在汽车系统中至关重要。这些系统的行为往往依赖于复杂的动力学以及随机行为。我们提出了一个概率扩展的时钟约束规约语言，称为PrCCSL，规范（非）功能性需求，并证明了需求的正确性，通过映射到UPPAAL模型的语义规范。以前的工作扩展在本文中，包括一个扩展的PrCCSL，称为PrCCSL*，规范的随机和动态系统的行为，以及复杂的要求相关的多个事件。为了形式化地分析PrCCSL* 中规定的系统行为/需求，将PrCCSL* 规范转换为随机UPPAAL模型以进行形式化验证。我们实现了一个自动翻译工具，即ProTL，它也可以使用UPPAAL-SMC作为分析后端对PrCCSL* 规范进行形式化分析。我们的方法证明了两个汽车系统的案例研究。
2019-10-31 cs.SE
A Formal Verification Technique for Architecture-based Embedded Systems in EAST-ADL
随着汽车嵌入式系统等软件密集型系统的复杂性显著增加，开发有质量保证的软件密集型系统是一项日益严峻的挑战。EAST-ADL是一种架构描述语言，旨在在安全关键汽车产品的开发中以多个抽象级别指定汽车嵌入式系统架构。在本文中，我们提出了一个基于架构的验证技术，增强了基于模型的开发过程中支持的EAST-ADL适应模型检查EAST-ADL规范。我们采用UPPAAL作为验证工具，以确保预测的功能行为的模型在EAST-ADL满足功能和实时要求。提出了基于体系结构的验证准则，并推导出符合该准则的转换规则。这使我们能够从EAST-ADL规范中提取相关信息，并生成可分析的UPPAAL模型。定义了EAST-ADL规范的形式化语义，这对EAST-ADL规范的自动验证至关重要。我们的方法是通过验证转向车系统单元的安全性来证明的。
2019-03-14 cs.SE
Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning
Microsoft Research（微软研究院）
该研究提出神经形式化验证（NFV），让AI编码智能体与成熟验证器结合，为主流语言开发者实现一键式程序验证，在Python编程问题数据集上取得了良好的验证效果。
2026-09-15 cs.PL cs.SE
ProofWright: Towards Agentic Formal Verification of CUDA
Georgia Institute of Technology（佐治亚理工学院）；NVIDIA Research（英伟达研究院）；Stanford University（斯坦福大学）
ProofWright 通过整合自动形式验证与 LLM 代码生成，为 CUDA 核心提供内存安全、线程安全和语义正确性保证，验证了 74% 的生成内核，发现传统测试遗漏的细微错误。
2026-03-18 cs.SE
Software is infrastructure: failures, successes, costs, and the case for formal verification
Université Paris Cité（巴黎西岱大学）；University of Malta（马耳他大学）；University of Southern Denmark（南丹麦大学）；King’s College London（伦敦国王学院）
本文探讨了软件在现代社会中的重要性及质量缺陷带来的成本，主张通过形式验证和程序分析来提升软件可靠性。
2026-01-29 cs.CY cs.SE
Formal Verification of Autonomous Vehicle Platooning
University of Sheffield（谢菲尔德大学）
预计在不久的将来，我们的高速公路上将有多辆自动驾驶汽车组成车队或车队。然而，在部署这样的车队之前，必须对这些车队中车辆的新自主行为进行认证。车辆排队的一个适当的表示是作为一个多智能体系统，其中每个代理捕获的“自主决策”进行的每辆车。为了保证车辆队列中的自主决策智能体不违反安全要求，我们使用了形式化验证。然而，由于用于验证代理代码的形式化验证技术不能扩展到整个系统，并且由于全局验证技术不能捕获自治行为的基本验证，因此我们使用两种方法的组合。这种混合策略使我们不仅可以验证系统模型的安全要求，还可以验证用于对自动驾驶汽车进行编程的实际代理代码的安全要求。
2016-02-04 cs.AI cs.SE
Towards Deriving Verification Properties
形式软件验证使用数学技术来确定软件具有某些属性。例如，软件系统的行为满足某些逻辑指定的属性。形式化方法有很长的历史，但是一个反复出现的假设是，要验证的属性是已知的，或者作为需求获取过程的一部分提供。本工作说明考虑的问题是：核查属性从何而来？它提出了一个系统地确定核查特性的程序。
2019-03-11 cs.SE
Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles
Faculty of Engineering, University of Porto（波尔图大学工程学院）；INESC TEC（TEC研究所）；INESC-ID（ID研究所）
本文利用LLMs和测试或acles自动为Dafny程序生成形式规范和验证注解，实验表明该方法在多数情况下有效，并展示了IDE集成的可行性。
2026-01-19 cs.SE
Causality and Responsibility for Formal Verification and Beyond
King's College London（伦敦国王学院）
由哈尔彭和珀尔定义的实际因果关系理论及其定量度量--责任度--在计算机科学的各个领域都被证明是非常有用的，因为它产生的结果与我们的直觉之间有很好的匹配。在本文中，我描述了因果关系的应用形式化验证，即解释反例，细化的覆盖度量，和符号轨迹评估。我还简要讨论了因果关系的法律推理的最新应用。
2016-08-29 cs.AI cs.SE
A Formal Verification Approach to Safeguard Controller Variables from Single Event Upset
本文提出一种结合程序分析与形式化验证的方法来识别条件相关变量，以减少单粒子翻转场景下的误报，并有助于编译器优化寄存器分配，从而降低控制器芯片成本。
2025-05-10 cs.SE
Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python
National Institute of Advanced Industrial Science and Technology（国家工业科学与技术研究院）
针对科研可重复性危机，提出Python统计程序形式验证框架。介绍Why3-py，将Python程序转为WhyML表示，还扩展StatWhy工具，可助用户识别假设及分析误用，验证程序正确性。
2026-09-22 cs.AI cs.LO cs.PL
Are Users More Willing to Use Formally Verified Password Managers?
本研究通过两项实验（15人形成性研究及200人定量研究）探究用户对形式化验证密码管理器的态度，发现用户视其为可取，并提出三项沟通改进建议。
2025-09-07 cs.CR cs.HC cs.LO
Formal verification of space systems designed with TASTE
基于模型的系统工程（MBSE）是一种开发方法，旨在构建正确的结构系统，提供了使用清晰，明确和完整的模型来描述它们沿着设计过程。该方法由几个自动化开发步骤的工程工具支持，例如代码，文档，测试用例等的生产。TASTE [1]是由ESA支持的实用MBSE工具集，它封装了几种技术来设计系统（数据建模，架构建模，行为建模/实现），自动生成二进制应用程序，并验证它。TASTE中的一个开放主题是系统设计的形式化验证。在本文中，我们描述了我们的方法的基础上，IF模型检查器[4]，使形式化验证的性质TASTE设计。欧空局MoC 4Space项目目前正在开发这种方法。
2021-11-19 cs.SE
Formal Verification of Consistency for Systems with Redundant Controllers
本文通过形式化验证发现冗余控制器算法NRP FD可能同时产生两个主控制器的一致性问题，并提出解决方案以增强系统鲁棒性与可靠性。
2024-03-27 cs.SE
Formal Verification of End-to-End Learning in Cyber-Physical Systems: Progress and Challenges
MIT-IBM Watson AI Lab（MIT-IBM沃森人工智能实验室）；IBM Research（IBM研究院）；Massachusetts Institute of Technology（麻省理工学院）
自动驾驶系统--如自动驾驶汽车、自动驾驶无人机和自动化列车--必须有强大的安全保障。在过去的十年中，基于形式化方法的技术在为大型软件系统（包括操作系统内核、加密协议和无人机控制软件）提供强正确性保证方面取得了一些成功。这些成功表明，通过构造正式的、计算机检查的正确性证明来确保自治系统的安全性是可能的。本文确定了现有的形式化验证技术的三个假设，解释了这些假设如何限制验证在自治系统中的适用性，并总结了初步工作，以提高形式化验证提供的证据的强度。
2020-06-15 cs.AI cs.LG cs.SE
Simulator Semantics for System Level Formal Verification
Sapienza University of Rome（罗马第一大学）
本文提出系统级形式验证中模拟器的正式语义，以解决模拟器行为未被形式化建模的问题，确保验证方法的正确性。
2015-09-24 cs.SE cs.SY eess.SY
Supporting Software Formal Verification with Large Language Models: An Experimental Study
本文提出 SpecVerify 框架，将 Claude 3.5 Sonnet 与 ESBMC 结合实现自动化形式化验证，在九个信息物理系统上达到 46.5% 准确率，并表明 LLM 可降低验证门槛但人机协作仍不可或缺。
2025-07-07 cs.SE
Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis
Shanghai Polytechnic University（上海理工大学）；Nanjing University of Science and Technology（南京理工大学）；Shanghai Jiao Tong University（上海交通大学）
研究针对zkEVM因实现错误可能破坏加密保证的问题，提出VeriSynth框架，通过大语言模型引导从Rust代码合成验证模型，采用混合范式及集成多种技术处理状态转换，在验证基准上错误检测率超90%，远超基线。
2026-07-23 cs.SE
Proceedings 8th International Workshop on Parallel and Distributed Methods in verifiCation
第八届并行和分布式验证方法国际研讨会（PDMC 2009）于2009年11月4日在埃因霍温理工大学举行，与正式方法2009和其他相关活动一起首次在正式方法周的标题下举行。本卷载有研讨会的最后会议记录。
2009-12-15 cs.CE cs.DC cs.LO
A System for Deduction-based Formal Verification of Workflow-oriented Software Models
研究了基于演绎方法的面向工作流软件模型的形式化验证。模型的行为的形式正确性被认为是。人工建立逻辑规范，这被认为是一组时态逻辑公式，似乎是一个没有经验的用户在应用演绎方法时的重大障碍。提出了一种基于演绎的面向工作流模型验证系统及其体系结构。推理过程基于语义表法，与传统的推理策略相比具有一定的优势。提出了一种自动生成逻辑规格说明的算法。生成过程基于BPMN的预定义工作流模式，BPMN是业务流程建模的标准和主导符号。该方法的主要思想是考虑模式，定义在时序逻辑方面，作为一种（逻辑）原语，使模型的转换构成一个逻辑规范的时序逻辑公式。自动化的生成过程是至关重要的，为弥合之间的差距的演绎推理的直观性和困难的实际应用的情况下，当逻辑规范是手动建立。这种方法已经在某种程度上支持了面向工作流模型的基于演绎的形式化验证，并有望增强我们对它的理解。
2014-12-31 cs.SE
VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees
Lund University（隆德大学）；Linköping University（林雪平大学）
本文提出训练后优化框架生成验证友好型神经网络（VNNs），在保持预测性能的同时提升形式化验证可行性，从而高效地为更多网络建立硬鲁棒性保证。
2024-06-10 cs.LG cs.SE
Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing
Formal Methods and Tools Lab, ISTI–CNR, Pisa, Italy（ISTI-国家研究委员会，意大利比萨）
本文基于Uppaal对合同自动机运行环境进行形式化建模、验证与测试，以提升开源分布式应用的可靠性。
2026-03-04 cs.FL cs.SE
Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering
Lancaster University（兰卡斯特大学）；Tsinghua University（清华大学）；Harbin Institute of Technology（哈尔滨工业大学）；Southwest University（西南大学）；Aarhus University（奥胡斯大学）；University of York（约克大学）
提出Forge管道，结合Vibe编码与模型驱动工程，通过多种形式化验证（Dafny、CSP、Isabelle）迭代修正LLM生成的Java代码，生成符合安全标准的验证证据。
2026-06-24 cs.FL cs.SE
Contribution to the Formal Specification and Verification of a Multi-Agent Robotic System
IRISA（法国国家信息与自动化研究所布列塔尼大西洋分部）；University of South Brittany（南布列塔尼大学）；The Islamia University of Bahawalpur（巴哈瓦尔布尔伊斯兰大学）
重要的是要有多智能体机器人系统规范，以确保正确性，安全性和活性。由于这些系统具有并发性，并且通常具有动态环境，因此这些系统的形式化规范和验证以及从抽象到具体概念的逐步细化在系统正确性中起着重要作用。形式化验证用于系统空间的详尽调查，从而确保排除行为中未检测到的故障。我们构建系统的子组件，基于软件体系结构的增量。挑战是开发一个安全的多智能体机器人系统，更具体地说，以确保安全性和活性的正确性。基于模型检测的形式化规约具有灵活性强、语法具体等特点，对多智能体机器人系统的正确性起着至关重要的作用。由于这类系统具有高并发性，且大多数情况下是动态的，因此形式化地验证其安全性和活性是非常重要的。我们已经考虑了一个案例研究的多智能体机器人系统的仓库之间的股票运输，以证明我们的正式方法。我们提出的开发方法允许在规范定义期间进行形式化验证。开发过程分为需求规范、验证规范、体系结构规范和实现四个主要阶段。
2015-10-02 cs.AI cs.MA cs.SE
SAT-based Formal Fault-Resistance Verification of Cryptographic Circuits
本文将密码电路抗故障验证问题形式化为NP完全问题，提出将其编码为布尔可满足性（SAT）问题并利用现成SAT求解器求解的方法，在开源工具FIRMER中实现了该方案，其实验验证效率与可扩展性显著优于现有方法。
2023-07-02 cs.AR cs.CR cs.SE
Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair
Independent Researcher Seattle, WA, USA
本文提出将LLM与开源形式化后端结合的多智能体RTL修复流水线，通过反例引导迭代实现RTL修复，经ALU案例及6基准测试验证可行性并分析失效模式。
2026-08-03 cs.AR cs.LG cs.SE
Emergent Formal Verification: How an Autonomous AI Ecosystem Independently Discovered SMT-Based Safety Across Six Domains
Aisophical SRL
自主AI生态系统在无显式形式方法指令下，独立在六个AI安全领域发现SMT求解器的应用，提出统一框架实现100%准确验证。
2026-03-22 cs.AI cs.MA cs.SE
Formal Verification Of A Shopping Basket Application Model Using PRISM
本文使用Prism Model Checker对购物篮应用模型进行形式化验证，模拟购物者在购物过程中的状态行为并分析可达性。
2023-07-16 cs.IT cs.SE math.IT
A Semi-Formal Verification Methodology for Efficient Configuration Coverage of Highly Configurable Digital Designs
Infineon Technologies（英飞凌科技）
本文提出一种结合仿真与形式化方法的半形式化验证方法，以降低运行时间并实现高度可配置数字设计的高配置覆盖率，并在微处理器IP上验证了其有效性。
2024-04-20 cs.AI cs.AR cs.SE
DafnyBench: A Benchmark for Formal Software Verification
Harvard College（哈佛学院）；Massachusetts Institute of Technology（麻省理工学院）；Northeastern University（东北大学）；Stanford University（斯坦福大学）；University of California Irvine（加州大学欧文分校）；Harvard University（哈佛大学）
本文提出最大的形式化软件验证基准 DafnyBench，评估 LLM 为 Dafny 自动生成验证提示的能力，并给出成功率及反馈重试、代码规模影响等基线结果。
2024-06-12 cs.AI cs.LG cs.PL
