Integrating Topological Proofs with Model Checking to Instrument Iterative Design
系统开发不是一个线性的、一次性的过程。它通过改进和修订进行。为了支持系统满足其需求的保证，最好在每个细化或修订步骤之后执行连续验证。为了实现实际应用，形式化系统建模和验证必须有效地支持持续验证。我们的建议，以解决这个问题是TOrPEDO，一种验证方法，模型通过部分Kripke结构（PKS）和要求指定为线性时间时序逻辑（LTL）属性。PKS支持细化，通过故意指示模型中稍后完成的未指定部分。我们支持两种互补形式的验证：通过模型检验和证明。模型检验可用于提供反例，即，查明违反需求的模型行为。相反，证明是有用的，因为它们可以解释为什么需求得到满足。在我们的工作中，我们引入了一个特定的概念证明，称为拓扑证明（TP）。一个TP产生一个切片的原始PKS证明财产满意度。因为模型可能是不完整的，所以TOrPEDO支持对需求满足、违反和可能满足的推理（在满足取决于未知部分的情况下）。
2018-11-26 cs.LO
Counterexample-Guided Abstraction Refinement for Generalized Graph Transformation Systems (Full Version)
本文针对图变换系统的可达性验证问题，提出结合抽象解释与反例引导抽象精化的自动验证方法，以有限近似处理无限状态空间，并将结果推广到一般反应式系统。
2025-04-11 cs.LO
Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction
本文研究了实时的【形】系统的安全性验证与综合问题。我们介绍实时的【形】程序，这些程序由可以执行离散和实值变量赋值的指令组成。它们足够通用，可以捕获有趣的时间系统类，如时间自动机，秒表自动机，时间（d）Petri网和混合自动机。我们提出了一种使用轨迹抽象细化的半算法来解决实时的【形】程序的可达性验证问题和参数综合问题。所有提出的算法已经实施，我们已经进行了一系列的实验，比较我们的新方法的性能，以国家的最先进的工具，在经典的可达性，鲁棒性分析和参数合成定时系统。我们表明，我们的新方法提供了解决方案，这些问题是无法解决的，目前最先进的工具。
2020-07-21 cs.FL cs.LO cs.SY
Refinement Reflection: Complete Verification with SMT
我们介绍了精化反射，一个新的框架，用于建立基于SMT的演绎验证。关键思想是将实现用户定义函数的代码反映到函数的（输出）细化类型中。因此，在使用函数时，函数定义以允许可判定验证的精确方式在SMT逻辑中实例化。反射允许用户通过使用模式匹配和递归来编写其他程序来编写程序的等式证明，以执行大小写分解和归纳。因此，通过命题作为类型的原则，我们表明，反射允许规范的任意功能的正确性属性。最后，我们介绍了一个证明搜索算法，称为证明逻辑评估，使用技术从模型检验和抽象的解释，完全自动化的等式推理。我们已经在Liquid Haskell中实现了反射，并使用它来验证Monoid，Applicationative，Functor和Monad类型类的广泛使用的实例实际上满足使客户端安全所需的关键代数定律，并使用反射构建了第一个库，该库实际验证了关于关联性和排序的假设，这些假设对于安全的确定性并行性至关重要。
2017-11-09 cs.LO cs.PL
Counterexample-guided Abstraction Refinement for POMDPs
University of Notre Dame（圣母大学）
本文提出针对POMDPs的反例引导抽象细化方法，设计了新的抽象系统模型和模拟关系，并开发了新的细化算法，以实现POMDPs的验证。
2017-03-10 cs.LO cs.SY eess.SY
Conditional Contextual Refinement (CCR)
上下文精化（CR）是指定开放程序的标准概念之一。CR有两个主要优点：（i）（水平和垂直）组合性，其允许我们将大的上下文细化分解成许多较小的细化，从而实现模块化和增量验证，以及（ii）对编程特征没有限制，从而允许，例如，相互递归、指针值传递和高阶函数。然而，CR有一个缺点，它不能对上下文施加条件，因为它量化了所有上下文，这确实在支持完整的组合性和编程特性方面发挥了关键作用。在本文中，我们解决的问题，找到一个概念的细化，满足所有三个要求：支持完整的组合性，完整的（顺序）编程功能，并在上下文丰富的条件。作为一种解决方案，我们提出了一种新的细化理论，称为CCR（条件上下文细化），并开发了一个验证框架的基础上，它允许我们模块化和增量验证一个具体的模块对一个抽象的模块分离逻辑风格的前和后条件下的外部模块。它在Coq中完全形式化，并提供了一种证明模式，该模式结合了（i）关于保留IO事件和终止等副作用的模拟推理和（ii）关于前置和后置条件的命题推理。此外，验证结果与CompCert相结合，使我们正式建立从顶级抽象程序的行为细化，一直到他们的汇编代码。
2022-03-14 cs.LO cs.PL
An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks
The Hebrew University of Jerusalem（耶路撒冷希伯来大学）；Stanford University（斯坦福大学）
卷积神经网络由于其在计算机视觉、图像处理等领域中的优异性能而获得了广泛的普及。不幸的是，现在众所周知，卷积网络经常产生错误的结果-例如，这些网络输入的微小扰动可能导致严重的分类错误。近年来，已经提出了许多验证方法来证明不存在此类错误，但这些方法通常适用于完全连接的网络，并且在应用于卷积网络时会遇到加剧的可扩展性问题。为了解决这一差距，我们在这里提出了Cnn-Abs框架，该框架特别针对卷积网络的验证。Cnn-Abs的核心是一种抽象-细化技术，它通过去除卷积连接来简化验证问题，这种方式可以完美地创建原始问题的过度近似;如果结果问题变得过于抽象，则恢复这些连接。Cnn-Abs旨在使用现有的验证引擎作为后端，我们的评估表明，它可以显着提高最先进的DNN验证引擎的性能，平均减少15.7%的运行时间。
2022-01-06 cs.CV cs.LG cs.LO
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine
我们正式验证一个抽象的机器调用的值的alcuda演算与de Bruijn条款，简单的替代，和小步语义。我们遵循逐步改进的方法，从一个带有替换的朴素堆栈机器开始。然后，我们细化到一个具有闭包的机器，最后是一个具有为闭包提供结构共享的堆的机器。我们证明了三个细化步骤的正确性与组成小步自下而上的模拟。有一个附带的Coq开发验证所有结果。
2019-01-02 cs.LO cs.PL
Verifying C11-Style Weak Memory Libraries via Refinement
演绎验证的并发程序在弱内存下，到目前为止，仅限于简单的程序在一个单一的状态空间。对于可伸缩性，我们还需要具有可验证库抽象的模块化技术。本文解决了这一挑战的背景下，RC 11 RAR，C11内存模型的一个子集，允许放松和释放获取访问，但不允许，所谓的，负载缓冲周期。我们开发了一个简单的框架，用于指定抽象对象，精确地描述了抽象方法调用的可观察性保证。我们展示了如何将这个框架与一个操作语义集成在一起，该操作语义可以验证客户端程序从他们使用的库中执行抽象方法调用。最后，我们将展示如何实现这样的抽象在RC 11 RAR可以验证通过开发一个（上下文）细化框架的抽象对象。我们的框架，包括操作语义，客户端库程序的验证技术，和抽象库和它们的实现之间的模拟，已在伊莎贝尔/HOL机械化。
2021-08-16 cs.LO cs.PL
A Practical Approach to Interval Refinement for math.h/cmath Functions
C++程序的验证已经在几个领域取得了相当大的进展，但对于使用这些语言的数学库的程序来说却没有。原因是，所有广泛使用的库都不能保证计算结果。这似乎阻止了对使用它们的程序进行形式化验证的任何尝试：没有函数的规范，就不能静态地得出关于程序行为的结论。我们提出一个投降的替代方案。我们引入了一种实用的方法，利用大多数math.h/cmath函数几乎是分段单调的这一事实：正如我们通过详尽测试发现的那样，它们可能会出现小故障，通常大小非常小，数量也很少。我们开发的间隔细化技术，这些功能的基础上修改的二分法搜索，使验证通过符号执行基于模型检验，抽象的解释，和测试数据生成。我们的细化算法是文献中第一个能够处理非正确舍入函数实现的算法，能够在最常见的实现中进行验证。我们实验评估我们的方法在现实世界的代码，显示其检测或排除异常行为的能力。
2020-08-11 cs.LO cs.PL cs.SE
Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement
LMU Munich（慕尼黑大学）
本文提出了一种基于并行轨迹抽象细化的多线程软件模型检查方法，通过利用多核CPU提升验证效率，优于传统顺序方法和DSS技术。
2026-01-15 cs.LO cs.PL cs.SE
Formal Modelling, Testing and Verification of HSA Memory Models using Event-B
HSA基金会已经制定了HSA平台系统架构规范，该规范在解决明确和一致的方法来指定弱一致内存的需求方面有很大的帮助。HSA是用自然语言指定的，这使得它对多种模糊的解释开放，并且可能在硬件和软件中实现它时出现错误。在本文中，我们提出了一个形式化的HSA模型，可用于并发软件应用程序的开发和验证，以及在开发和验证的HSA兼容平台本身。我们使用Event-B语言来建立一个可证明正确的层次结构的模型，从最抽象的HSA接近实现级别的详细细化。我们的内存模型是通用的，因为它们代表了任意数量的主机，程序和指令交织。我们使用精化来推理这样的一般模型。使用罗丹工具，我们能够建模和验证整个层次的模型使用证明，以建立每个细化是正确的。我们定义了一个自动化的验证方法，使我们能够测试模型的基线符合性对一套已发布的HSA石蕊测试。一旦我们完成了模型验证，我们开发了一个覆盖率驱动的方法，从事件B模型和用户指定的覆盖率模型中提取更丰富的测试集。这些测试用于硬件和软件系统的广泛回归测试。我们的方法的细化为基础的正式建模，基线符合性测试的模型和覆盖率驱动的测试提取使用单一的语言的事件-B是一种新的方式来解决所面临的一个关键挑战的设计和验证的多核系统。
2016-05-16 cs.LO cs.SE
Model Sketching by Abstraction Refinement for Lifted Model Checking (Extended Version)
在这项工作中，我们展示了如何使用验证和分析技术的模型家庭（软件产品线）的数字功能提供了一个有趣的技术，合成完整的模型从草图（即\具有孔的部分模型）。特别是，我们提出了一种方法，用于合成Promela模型草图使用特定于变量的抽象细化解除（基于家庭）模型检验。
2021-12-21 cs.LO cs.PL
Exploiting Hierarchy in the Abstraction-Based Verification of Statecharts Using SMT Solvers
在基于状态的系统设计中，状态图经常被用作建模形式。形式化验证技术也经常用于证明系统行为的某些属性。形式化验证最有效的技术之一是反例引导的抽象精化（CEGAR），它通过自动构建和精化抽象来降低系统的复杂性。在我们的论文中，我们提出了一种新的适应CEGAR方法层次状态图模型。首先，我们引入一个编码的状态图的逻辑公式，保留有关的状态层次结构的信息。基于这种编码，我们提出了抽象和细化技术，这些技术利用状态图的分层结构，并处理模型中的变量。编码使我们能够使用SMT求解器的系统的探索和验证的抽象模型，也包括有界模型检验。我们证明了我们的抽象技术的适用性和效率与测量行业的动机的例子。
2017-03-21 cs.LO cs.SE
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
On the Verification of a WiMax Design Using Symbolic Simulation
在自顶向下的多层次设计方法中，在更高抽象层次上的设计描述被逐步细化到最终实现。基于仿真的技术传统上被用于验证这种模型改进不会改变设计功能。不幸的是，利用计算机模拟，不可能在合理的时间内完全检查设计变换是否正确，因为这样做所需的测试模式的数量随着系统状态变量的数量呈指数级增加。在本文中，我们提出了一种方法，用于验证在设计过程中产生的模型在更高的抽象层次的设计规范的一致性。我们使用递归方程的序列建模系统的行为。然后，我们使用符号模拟与等价性检查和属性检查技术的设计验证。使用我们提出的方法，我们已经验证了三个WiMax系统模型在不同层次的设计抽象的等效性，以及这些模型上的各种系统属性的正确性。我们的符号建模和验证实验表明，所提出的验证方法提供了其数值对应的性能优势。
2013-07-31 cs.LO
Incremental Database Design using UML-B and Event-B
许多关键系统的正确操作依赖于底层数据库的数据一致性和完整性属性。因此，一个可验证的和严格的数据库设计过程是非常可取的。本研究的目的是调查和提供一个全面和实用的方法，通过分层细化正式的方法建模数据库。该方法是由一些案例研究，使用UML-B的抽象和细化和验证与罗丹工具的指导。UML-B是Event-B形式主义的图形表示，Rodin工具支持Event-B和UML-B的验证。我们的方法指导开发人员通过分层细化在UML-B中建模关系数据库，并指定数据库上的必要约束和操作。
2018-05-15 cs.DB cs.LO cs.SE
Refinement orders for quantum programs
Tsinghua University（清华大学）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）
本文研究了量子程序的细化顺序，揭示了不同规范类型与经典域论概念的对应关系，以及确定性和非确定性程序的细化特性。
2026-02-19 cs.LO quant-ph
Temporal logic control of general Markov decision processes by approximate policy refinement
California Institute of Technology（加州理工学院）；School of Computing, Newcastle University（纽卡斯尔大学计算机学院）；Computer Science Department, Oxford University（牛津大学计算机科学系）
本文研究了如何利用近似概率关系在一般马尔可夫决策过程上实现正确-by-设计的时序逻辑控制，通过在抽象模型上进行计算，确保在抽象模型上满足的属性在原始模型上也能通过细化的控制策略得到满足。
2018-11-27 cs.LO cs.SY eess.SY
Formal that "Floats" High: Formal Verification of Floating Point Arithmetic
1 Infineon Technologies Semiconductor India Private Limited, India 2 Infineon Technologies Dresden AG \& Co. KG, Germany
本文提出了一种基于代理AI的形式化验证方法，通过直接RTL到RTL模型检查和黄金参考模型验证浮点运算，结合AI生成属性和人机协作细化，提升验证效率和覆盖范围。
2025-12-07 cs.AI cs.AR cs.LO
Skipping Refinement
我们引入跳跃细化，一个新的概念的正确性推理优化反应系统。使用精化对反应式系统进行推理涉及定义抽象的高级规范系统和具体的低级实现系统。然后，我们可以看到，实现所允许的每一个行为也都是规范所允许的。由于抽象级别的差异，通常情况下，实现需要许多步骤来匹配规范的一个步骤，因此，直接考虑口吃对于细化非常有用。然而，一些优化的实现实际上可以一次执行多个规范步骤。例如，存储器控制器可以将命令缓冲到存储器，并且在稍后的时间同时更新多个存储器位置，从而跳过抽象规范的若干可观察状态，这一次仅更新一个存储器位置。我们引入跳跃仿真细化，并提供了一个健全和完整的表征组成的“本地”证明规则，适合机械化和自动化验证。我们目前的案例研究，突出跳过细化的适用性：JVM启发堆栈机，一个简单的内存控制器和标量向量编译器转换。我们的实验结果表明，目前的模型检查和自动定理证明工具很难自动分析这些系统使用现有的概念的正确性，但他们可以分析系统，如果我们使用跳过细化。
2015-02-10 cs.LO cs.PL
SCJ-Circus: a refinement-oriented formal notation for Safety-Critical Java
安全关键Java（Safety-Critical Java，SCJ）是Java的一个版本，其目标是支持实时，嵌入式，安全关键软件的开发。特别是，SCJ通过引入实施更简单的体系结构和更简单的并发和内存模型的抽象来支持此类软件的认证。在本文中，我们提出了SCJ-Circus，一个面向细化的正式符号，支持规范和验证的低级别的编程模型，包括SCJ引入的新的抽象。SCJ-Circus是状态丰富进程代数Circus家族的一部分，因此，SCJ-Circus包括Circus结构，用于建模顺序和并发行为，实时和面向对象。我们在这里提出的语法和语义的SCJ-Circus，这是定义映射SCJ-Circus结构的标准Circus。这是基于现有的方法建模SCJ程序。我们还扩展了现有的马戏团为基础的细化策略，目标SCJ程序占SCJ马戏团模型的生成接近SCJ的实现。
2016-06-07 cs.LO cs.PL cs.SE
