Safety Verification for Neural Networks Based on Set-boundary Analysis
National University of Defense Technology（国防科技大学）
神经网络（NN）越来越多地应用于安全关键系统，如自动驾驶汽车。然而，他们是脆弱的，往往是不守规矩的。因此，在实际部署之前，他们的行为必须经过严格的保证。在本文中，我们提出了一个集边界可达性方法，从拓扑的角度来研究神经网络的安全性验证问题。给定一个具有输入集和安全集的神经网络，安全验证问题是确定由输入集产生的神经网络的所有输出是否都落在安全集内。在我们的方法中，主要利用了神经网络的同胚性质，它建立了一个映射边界到边界的关系。利用这一特性，通过提取输入集的子集而不是整个输入集来促进可达性计算，从而控制可达性分析中的包裹效应，并促进减少安全验证的计算负担。同胚性质存在于一些广泛使用的神经网络，如可逆神经网络。值得注意的表示是可逆残差网络（i-ResNets）和神经常微分方程（Neural ODE）。对于这些神经网络，我们的集边界可达性方法只需要在输入集的边界上执行可达性分析。对于不具有此属性的输入集的NN，我们探索的输入集的子集建立本地同胚属性，然后放弃这些子集的可达性计算。最后，一些例子证明了所提出的方法的性能。
2022-10-09 cs.AI cs.LG cs.SE
Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems
屏障证书是一种归纳不变函数，可用于混合系统的安全验证。基于屏障证书的安全验证避免了非线性混合系统难以求解的精确可达集的显式计算。本文提出了一种新的屏障证书条件，称为指数条件，用于半代数混合系统的安全性验证。指数条件最大的优点是它比现有的凸条件具有更低的保守性，同时又具有凸性。一方面，一个不太保守的屏障证书形成了一个更严格的过度近似的可达集，因此能够验证关键的安全属性。另一方面，凸性的性质保证了半定规划方法的可解性。最后通过实例说明了该方法的有效性和实用性。
2013-03-27 cs.SE math.OC
Heterogeneous Runtime Verification of Safety Critical Cyber Physical Systems
先进的嵌入式系统技术是信息物理系统（CPS）应用快速增长的关键驱动力之一。网络物理系统由多个协调和合作的组件组成，这些组件通常是软件密集型的，并且相互交互以实现前所未有的任务。这种复杂的CPS有多个攻击面和攻击向量，我们必须防范。为了实现这一目标，我们展示了一个多层次的运行时安全和安全监控框架，其中有监视器在CPS的检测和隔离的攻击。我们使用基于流的运行时验证工具TeSSLa在FPGA上实现了运行时监视器。我们展示了我们的监测方案的自动紧急制动（AEB）CPS系统。
2020-09-20 cs.SE
Exact Safety Verification of Hybrid Systems Using Sums-Of-Squares Representation
在本文中，我们讨论了如何产生归纳不变量的安全验证的混合系统。提出了一种计算系统不等式归纳不变量的符号-数值混合方法。给定系统的数值不变量可以通过求解一个参数化多项式优化问题，通过平方和（SOS）松弛。采用高斯-牛顿加细和有理向量恢复的方法得到了满足不变量条件的有理系数不变量。给出了几个例子来说明我们的算法。
2011-12-11 cs.SE math.OC
Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study (extended version)
本文提出一种符合功能安全标准的 PLC 程序形式化验证即服务，通过外部专家降低组织内部培训成本，并扩展至时间相关及专有技术保护组件建模，在 CERN 与 GSI 粒子加速器安全关键装置中验证了其有效性。
2025-02-26 cs.LO cs.SE
Safety Verification and Optimization in Industrial Drive Systems
针对工业驱动系统安全与诊断挑战，本文利用Uppaal Stratego对BDM建模验证并强化学习优化，将安全故障分数提升至90%阈值，增强故障检测能力。
2025-03-27 cs.SE
Verification of Component Fault Trees Using Error Effect Simulations
安全相关系统的日益复杂性导致安全保证的努力日益增加。因此，在保证安全运行的同时，降低开发成本和缩短上市时间是一项重大挑战。为了使有效的安全评估复杂的架构，我们提出了一种方法，它结合了演绎安全分析，在组件故障树（CFTs）的形式，与错误效应模拟（EES）的健全检查。这种组合减少了两种分析的缺点，例如在CFTs中主观的故障传播假设或EES相关故障场景的确定。CFT和EES均提供模块化、可重复使用和组合安全分析，并适用于整个设计过程。它们支持持续的模型改进和重复使用已进行的安全分析和仿真模型。因此，可以在早期设计阶段识别违反安全目标的行为，并且重新使用进行的安全分析可以减少安全评估的开销。
2021-06-07 cs.SE
Exact Safety Verification of Hybrid Systems Based on Bilinear SOS Representation
在本文中，我们解决的问题，非线性混合系统的安全性验证。提出了一种有效计算混合系统精确不等式不变量的符号-数值混合方法。首先通过PENBMI求解器或迭代法求解一类双线性SOS规划问题，得到混合系统的数值不变量，然后利用修正的Newton加细和有理向量恢复技术，得到了{ \it exactly}满足不变量条件的有理系数多项式精确不变量.在一些基准测试上的实验表明了算法的有效性。
2012-09-25 cs.SC cs.SE
Offline Runtime Verification of Safety Requirements using CSP
University of Liverpool（利物浦大学）；Maynooth University（梅努斯大学）
动态形式化验证是一种关键工具，用于提供系统在使用时满足其要求的持续信心，特别是在系统使用前与静态形式化验证配合使用时。本文介绍了一个工作流和验证（RV）工具链，Varanus，以及它们在工业案例研究中的应用。使用工作流，我们手动从自然语言的安全要求文档中导出一个通信顺序进程（CSP）模型，Varanus将其用作监视器Oracle。这种模型的重用意味着监视器预言机不必单独开发，否则会冒着它和静态验证模型之间不一致的风险。这种方法是由一个远程操作系统，称为MASCOT，它使远程操作内的联合欧洲环（JET）聚变反应堆的离线RV证明。我们描述了我们的MASCOT安全设计文件模型（包括建模过程如何揭示设计中的规格不足），并评估了Varanus工具链的实用性。工作流程和工具提供了安全文件的确认、从文件到系统的安全属性的可追溯性以及RV的经验证的oracle。
2021-05-25 cs.FL cs.RO cs.SE
Quantifying Uncertainty in FMEDA Safety Metrics: An Error Propagation Approach for Enhanced ASIC Verification
Robert Bosch GmbH（罗伯特·博世有限公司）
本文提出利用误差传播理论量化FMEDA安全指标的不确定性，通过提供SPFM和LFM的最大偏差和置信区间，提升安全分析质量，并引入误差重要性标识符指导改进，增强FMEDA的透明度和可信度。
2026-03-25 cs.AR cs.SE
Generating Automotive Code: Large Language Models for Software Development and Verification in Safety-Critical Systems
Technical University of Munich（慕尼黑技术大学）
本文提出将生成式AI与大语言模型集成到汽车软件开发生命周期的新框架，通过静态验证、测试驱动开发和迭代细化实现安全关键代码自动生成，并以自适应巡航控制系统验证其合规性与可靠性。
2025-06-04 cs.AI cs.SE
Industrial-Strength Verification of Solid State Interlocking Programs
现代联锁的日益复杂性对确保铁路安全提出了重大挑战。这就要求应用形式化的方法来保证和验证它们的安全性.我们已经开发了一个行业强度的工具集，称为SafeCap，用于联锁的形式化验证。我们的目标是克服在工业中部署正式方法的主要障碍。提出的方法验证联锁数据开发的信号工程师的方式，他们是由行业设计的。它确保使用最先进的技术（自动定理证明器和求解器）对安全属性进行全自动验证，并根据工程师使用的符号提供诊断。在过去的两年中，SafeCap已成功用于验证26个真实的干线联锁，这些联锁由不同的供应商和设计办公室开发。SafeCap目前用于咨询，通过提供额外的验证级别和能够更早地发现错误来补充人工检查和测试过程。我们现在正在开发一个安全案例，以支持将其用作其中一些活动的替代方案。
2022-01-14 cs.SE
Event-based Formalization of Safety-critical Operating System Standards: An Experience Report on ARINC 653 using Event-B
标准在安全关键系统中发挥着关键作用。标准中的错误可能会误导系统开发人员的理解，并将错误引入系统实现。在本文中，我们提出了一个事件B的形式化和验证的ARINC 653标准，它提供了一个标准化的接口之间的安全关键的实时操作系统和应用软件，以及一组功能，旨在提高安全和认证过程中的安全关键系统。该形式化模型是ARINC 653的一个完整模型，为符合ARINC 653规范的操作系统和应用程序的形式化开发和验证提供了必要的基础。六个隐藏的错误被发现从使用事件B形式推理方法的验证。
2015-09-10 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
Safety Verification and Refutation by k-invariants and k-induction (extended version)
大多数软件验证工具都可以归类为许多已建立的系列之一，每个系列都有自己的重点和优势。例如，模型检验中的具体反例生成、抽象解释中的不变推理和演绎验证中的注释完备性等。这就产生了一个重要的和基本的可用性问题，因为用户可能不得不学习和使用一种技术来发现潜在的问题，但随后需要一种完全不同的技术来表明它们已经被修复。本文提出了一个统一的算法kIkI，它严格地推广了抽象解释、有界模型检验和k-归纳法。这不仅结合了这些技术的长处，而且使它们能够相互作用和相互加强，从而提供了一种“单一工具”的核查方法。
2015-06-29 cs.LO cs.SE
Safely Entering the Deep: A Review of Verification and Validation for Machine Learning and a Challenge Elicitation in the Automotive Industry
深度神经网络（DNN）将成为汽车软件工程的基石。然而，使用DNN开发系统为安全评估带来了新的挑战。本文综述了基于机器学习的安全关键系统验证和确认的最新进展。此外，我们在瑞典与汽车专家一起举办了一系列关于DNN的感知研讨会，证实ISO 26262在很大程度上违反了DNN的性质。我们建议航空航天到汽车的知识转移和基于系统的安全方法，例如，安全笼架构和模拟系统测试用例。
2018-12-13 cs.SE
Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification
本文首次实证研究用于内存安全验证的单元证明，提出结合验证反馈与客观标准的系统化构建方法，并在四个嵌入式操作系统上验证其有效性与成本。
2025-03-17 cs.SE
Verifying the Safety of a Flight-Critical System
本文介绍了我们的工作演示验证技术的飞行关键系统的现实功能，大小和复杂性。我们的工作针对一个商用飞机控制系统命名为运输类模型（TCM），并涉及几个阶段：形式化和消除歧义的要求，与主专家合作;处理模型，他们使用的形式化验证工具;应用组合技术在体系结构和组件级别的规模验证。在一个重要的NASA里程碑的背景下进行，这项研究的形式化验证在实践中是最具挑战性的，我们的团队已经执行，它花了几个人月来完成it. This本文介绍了我们遵循的方法和我们学到的教训。
2015-02-09 cs.SE
A Survey of Analysis Methods for Security and Safety verification in IoT Systems
物联网（IoT）在过去几年中在所有生活学科中迅速发展。物联网为不同领域的用户提供自动化和智能控制，如家庭自动化、医疗保健系统、汽车等。鉴于连接的物联网设备数量巨大，这种增长导致其环境中相当大的物联网应用程序之间的大量自动交互，使物联网应用程序更智能，用户更愉快。但是，物联网应用程序的一些不可预见的交互和任何潜在的恶意行为都可能对其用户造成严重的不安全和不安全后果，主要是非专家，他们缺乏关于物联网自动化过程潜在影响的必要知识。在本文中，我们研究了物联网系统的安全性和安全验证问题。我们调查了利用程序分析来验证物联网应用程序的安全性和安全属性的技术。该研究提出了一套分类和分类属性，以提高我们对这一领域的研究景观的理解。此外，我们还讨论了调查工作中考虑的主要挑战以及可以采用的潜在解决方案，以确保物联网系统的安全性。
2022-03-03 cs.CR cs.SE
Testing and verification of neural-network-based safety-critical control software: A systematic literature review
Norwegian University of Science and Technology（挪威科技大学）；Southwest Jiaotong University（西南交通大学）
背景：神经网络（NN）算法已经成功地应用于许多安全关键的网络物理系统（SCCPS）。基于神经网络的控制软件的测试与验证（T&V）是软件工程和安全工程研究者和实践者关注的热点。目的：随着对基于神经网络的控制软件在安全关键领域的T&V研究的增加，重要的是系统地回顾最先进的T&V方法，对发明的方法和工具进行分类，并确定未来研究的挑战和差距。方法：检索950篇关于神经网络安全关键控制软件（SCCS）测试与验证的文献。为了达到我们的结果，我们过滤了2001年至2018年期间发表的83篇主要论文，应用主题分析方法分析了从选定论文中提取的数据，介绍了方法的分类，并确定了挑战。结论：这些方法分为五个高阶主题：确保神经网络的鲁棒性，确保基于神经网络的控制软件的安全性，提高神经网络的故障恢复能力，测量和确保测试的完整性，提高神经网络的可解释性。从行业的角度来看，提高NN的可解释性是安全关键型应用的关键需求。我们还调查了四个主要安全生命周期阶段中的九个安全完整性属性，以调查IEC 61508-3中T&V目标的实现水平。结果表明，正确性、完整性、无内在错误和容错是研究界最关注的问题。然而，很少的努力已经投入到实现可重复性，没有审查的研究集中在精确定义的测试配置或对常见原因故障的防御。
2020-03-20 cs.LG cs.SE cs.SY
Confidence Composition for Monitors of Verification Assumptions
University of Pennsylvania（宾夕法尼亚大学）；Rensselaer Polytechnic Inst.（伦斯勒理工学院）
具有神经网络控制器的信息物理系统的闭环验证在某些假设下提供了强有力的安全保证。然而，很难确定这些保证是否适用于运行时间，因为验证假设可能会被违反。为了预测已验证系统中的安全违规行为，我们提出了一个三步置信组合（CoCo）框架，用于监控验证假设。首先，我们用一个命题逻辑公式在假设上表示了可验证安全性的充分条件。其次，我们建立校准的信心监测器，评估每个假设成立的概率。第三，我们通过使用适合于逻辑公式的组合函数组合假设监视器来获得验证保证的置信度。我们的CoCo框架提供了理论界的成分监测器的校准和保守性。两个案例研究表明，成分监测校准比他们的成分，并成功地预测安全违规行为。
2022-05-05 cs.AI cs.LO cs.SE
Towards Verifying Safety Properties of Real-Time Probabilistic Systems
在基于形式方法的安全关键软件开发中使用概率已经引起了学术界和工业界的兴趣。我们通过我们的模型驱动的反应系统的工程方法空间和它的工具集反应块，提供了一个扩展，以支持建模和验证的实时的【形】行为，解决这一问题。该方法有利于从可重用的构建块组成系统模型，以及功能和实时的【形】属性的验证和Java代码的自动生成。在本文中，我们描述了扩展的工具集，使建模和验证的概率实时的【形】系统行为的空间属性，确保系统安全的重点。特别是，我们将概率行为的描述纳入到我们的反应块模型中，并集成了模型检查器PRISM，它允许验证实时的【形】系统满足特定的安全属性与给定的概率。此外，我们考虑的概率系统规格的空间含义，通过整合空间验证工具BeSpaceD，并给出了一个自动的方法来翻译系统规格的输入语言的PRISM和BeSpaceD。通过一个例子突出了这种方法。
2014-04-03 cs.SE
Supporting the monitoring of the verification process of critical systems'software
关键软件系统由于其操作环境的原因，在安全性、可靠性和可靠性方面面临着严格的要求。由于硬件与软件密集型部署的集成，安全性和安全性多年来逐渐变得重要，这引入了额外的错误源。因此，有必要遵循高质量的详尽的软件开发过程，除了必要的开发活动，以提高安全性和安全性，还集成技术，以提高软件开发过程本身的可靠性。然而，在实践中，使用自动化技术核查核查进程的情况并不十分普遍。这主要是由于所需技术成本高，而且在适应不同的规范和条例时很复杂。这项工作提出了一种全面管理验证过程的方法;该方法允许工程师监测和控制有关适用标准的项目状态。这种方法已通过在工具中的实现及其在实际项目中的应用得到验证。
2015-12-15 cs.SE
A Verification Methodology for Safety Assurance of Robotic Autonomous Systems
Faculty of Science and Technology, Norwegian University Of Life Sciences (NMBU)（科学与技术学院，挪威生命科学大学）；Department of Mechatronics, University of Agder (UiA)（机械电子系，阿格德大学）；Department of Computer Science, University Of York, UK（计算机科学系，约克大学（英国））
本文提出一种覆盖全生命周期的验证方法，通过危险分析、风险评估和形式化建模，在农业机器人上验证安全关键属性，促进设计问题早期识别。
2025-10-15 cs.FL cs.RO 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
Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security
本文首次对 Zephyr RTOS 并发内存管理进行形式化规范与机械化证明，扩展 PiCore 框架以验证完整性，并在功能验证中发现 C 实现中的三个缺陷。
2023-09-17 cs.SE
Agent-Driven Verification of Memory Safety for liblzma Decoder Components with VST
GenProof；IMDEA Software Institute（IMDEA软件研究所）
该研究基于VST，通过AI智能体辅助验证了liblzma生产级C解码器组件的内存安全，发现了其中的未定义行为，并解决了智能体驱动形式化验证的相关工程问题。
2026-09-01 cs.SE
Containment Verification: AI Safety Guarantees Independent of Alignment
AI Innovation Institute, Stony Brook University（石溪大学人工智能创新研究所）
本文提出包含性验证，通过代理框架本身提供安全保证。通过前向模拟细化和Dafny机制化，证明了在模型类型动作边界内对所有AI输出的边界策略强制性，首次实现了代理框架的演绎形式验证。
2026-07-01 cs.AI cs.CR cs.SE
Formal Verification of a Fail-Operational Automotive Driving System
用于高度自动化驾驶的故障操作系统即使在出现故障的情况下也必须完成驾驶任务。这需要冗余架构和在故障情况下重新配置系统的机制。因此，使用仲裁逻辑。为了功能安全，必须在出现任何电气和电子故障的情况下切换到回退水平。为了提供符合ISO 26262的安全论证证据，必须验证仲裁逻辑。验证过程提供了正确故障反应的确认，并且没有非预期的系统状态。传统的安全分析，如失效模式和效应分析，在这方面有其局限性。我们提出了一种基于形式化验证的分析方法，特别是模型检验，以验证驱动系统的故障操作行为。出于这个原因，我们对系统行为和相关架构进行建模，并正式指定安全需求。分析范围根据ISO 26262的要求定义。我们验证了符合行业标准的高度自动化驾驶的故障操作仲裁逻辑。我们的研究结果表明，在汽车故障操作驾驶系统的安全评估的正式方法可以成功地应用。我们能够检测到其他分析所忽略的故障，从而有助于安全关键功能的开发。
2021-01-18 cs.SE cs.SY eess.SY
Towards the Verification of Safety-critical Autonomous Systems in Dynamic Environments
TU Clausthal（克劳斯塔尔工业大学）
在高度异构的动态环境中部署自主系统的必要性越来越大，例如医院中的服务机器人或高速公路上的自动驾驶汽车。由于这些环境中的不确定性，在设计时获得的关于系统和环境模型的验证结果可能无法转移到运行时间的系统行为。对于在动态环境中运行的自主系统，运动安全和避免碰撞是关键要求。关于这些要求，Macek等人[6]定义了被动安全属性，该属性要求在自主系统移动时不会发生碰撞。为了验证这个属性，我们采用了两个阶段的过程相结合的静态验证方法，在设计时使用，与动态的，在运行时间。在设计阶段，我们利用UPPAAL形式化的自治系统及其环境的时间自动机和TCTL公式的安全属性，并验证这些模型的正确性与此属性。对于运行时阶段，我们构建了一个监视器来检查在设计时所做的假设在运行时间是否也是正确的。如果当前系统对环境的观测与初始系统假设不一致，则监控器向系统发送反馈，系统进入被动安全状态。
2016-12-15 cs.CY cs.RO cs.SE
Verification of interlocking systems using statistical model checking
在铁路领域，联锁是通过控制其活动元件（如信号机或道岔）来确保车站内训练交通安全的系统。现代联锁使用特定数据（称为应用数据）进行配置，这些数据反映了轨道布局并定义了联锁可以采取的操作。因此，训练交通的安全性依赖于应用数据的正确性，它们内部的错误可能导致安全问题，例如脱轨或碰撞。鉴于这一系统要求高度安全，其核查是一个关键问题。除了安全性，联锁还必须确保满足可用性属性，即没有训练会永远停在车站。大部分的研究处理这种验证依赖于模型检验。然而，由于状态空间爆炸的问题，这种方法不适合大型站。最近，提出了一种离散事件模拟方法，将验证限制在一组可能的场景中。模拟能够验证较大的台站，但没有证据表明模拟涵盖了所有有趣的场景。在本文中，我们采用了中间统计模型检验方法，提供了模型检验和仿真的优点。即使没有获得详尽性，统计模型检验也会以可参数化的置信度评估整个系统的可靠性和可用性。
2017-08-04 cs.SE
TAPInspector: Safety and Liveness Verification of Concurrent Trigger-Action IoT Systems
触发动作编程（TAP）是一种流行的最终用户编程框架，可以通过简单的触发动作规则简化物联网（IoT）自动化。但是，它也带来了新的安全威胁。已经提出了许多先进的技术来解决这个问题。严格推理基于TAP的物联网系统的安全性需要针对规则语义和物理世界特征的定义良好的模型和验证方法，例如，并发性、规则延迟、扩展操作、延迟属性和基于连接的规则交互，这些到目前为止一直缺少。通过分析这些特征，我们发现了9种新的规则交互漏洞，并在两个商业物联网平台上进行了验证。然后，我们提出了TAPInspector，这是一种新的系统，可以在并发的基于TAP的物联网系统中检测这些交互漏洞。它自动从物联网应用中提取TAP规则，通过模型切片和状态压缩将其转换为混合模型，并执行具有各种安全性和活性属性的语义分析和模型检验。我们的实验证实了TAPInspector的实用性：它从1108个真实市场的物联网应用程序中识别出533个与规则交互相关的违规行为，并且比没有优化的基线快至少60000倍。
2022-05-06 cs.CR cs.HC cs.NI
CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness
Université Paris-Saclay（巴黎-萨克雷大学）；CEA（法国原子能和替代能源委员会）；List（List实验室）
我们介绍CAISAR，一个正在积极开发的开源平台，用于表征AI系统的鲁棒性和安全性。CAISAR提供了一个统一的入口点，通过使用WhyML定义验证问题，Why3验证平台的成熟和表达语言。此外，CAISAR编排和组成了最先进的机器学习验证工具，这些工具单独使用无法有效地处理所有问题，但共同使用可以覆盖越来越多的属性。我们的目标是协助，一方面，V\&V过程中，通过减少选择的方法，适合于一个给定的验证问题的负担，另一方面，工具开发人员通过分解有用的功能，可视化，报告生成，属性解释，在一个平台。CAISAR将很快在https://git.frama-c.com/pub/caisar上提供。
2022-06-21 cs.AI cs.LO cs.NE
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
HarnessLLM: Rust Verification Harness Generation with Large Language Models
Ant Group（蚂蚁集团）
研究针对Rust代码内存安全验证开发验证框架难的问题，提出HarnessLLM自动化工作流程，利用大语言模型从测试套件生成框架，经实验评估效果良好，能检测内存安全漏洞，是首个用大语言模型为Rust项目内存安全验证生成框架的工作。
2026-07-27 cs.CR cs.SE
Applying Model Checking to Highly-Configurable Safety Critical Software: The SPS-PPS PLC Program
许多粒子加速器的一个重要方面是不断发展和频繁的配置变化，需要执行它们设计的实验。这通常会导致可配置软件的设计，可以吸收这些变化，并执行所需的控制和保护行动。这种设计策略最大限度地降低了工程和维护成本，但它使软件验证活动更具挑战性，因为必须保证任何可能的配置的安全属性。软件模型检验是一种广泛应用的自动化验证技术。这种验证方法探索系统模型的所有可能组合，以保证其符合某些属性或规范。这对于高度可配置的软件来说是一种非常合适的技术，因为通常有大量的组合需要检查。本文介绍了如何PLCverif，欧洲核子研究中心的模型检验平台，已被应用到一个高度可配置的可编程逻辑控制器（PLC）程序，SPS人员保护系统（PPS）。这种验证方法的好处和挑战也进行了讨论。
2022-03-30 cs.SE cs.SY eess.SY
Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars
本研究形式化自动驾驶的RSS模型，用KeYmaera X证明其纵向安全性，并通过精化与编译保持安全属性，最终生成可测试的Python代码。
2023-05-15 cs.LO cs.SE cs.SY
