Model-Checking of Linear-Time Properties Based on Possibility Measure
利用可能性测度研究了可能性Kripke结构下的LTL模型检验。首先介绍了可能性Kripke结构的概念和相关的可能性测度，然后研究了有限可能性Kripke结构线性时间可达性和重复可达性的模型检验.引入了可能性Kripke结构的标准安全性和非正则性，深入研究了正则安全性和非正则性的有限自动机验证问题。证明了有限可能性Kripke结构中正则安全性和非正则性的验证可以转化为本文所介绍的乘积可能性Kripke结构中可达性和重复可达性的验证。文中给出了几个算例来说明本文所提出的方法。
2016-09-25 cs.LO
Interpolation Properties and SAT-based Model Checking
Craig插值是一种广泛应用于验证的方法，具有重要的应用，如谓词抽象，反例引导的抽象精化和使用插值的懒惰抽象。大多数国家的最先进的模型检验技术的基础上插值需要插值集合，以满足特定的属性，我们称之为“集体”，他们不持有一般的所有插值系统，并建立了每个特定的系统和验证环境。然而，没有系统的方法存在，相互关联的个别插值系统和比较必要的集体。本文提出了一个统一的框架，其中包括（和概括）最常见的集体利用验证。我们用它来系统地研究集体和他们提出的约束条件，命题插值系统中使用的基于SAT的模型检验。
2013-06-21 cs.LO
Model Checking as Program Verification by Abstract Interpretation (Extended Version)
本文提出将模型检验视为程序验证，引入MOKA语言把时序逻辑公式编码为程序，并结合抽象解释与局部完全抽象动态精化分析精度，从而复用更一般的抽象并避免误报。
2025-06-05 cs.LO
Integrating Topological Proofs with Model Checking to Instrument Iterative Design
系统开发不是一个线性的、一次性的过程。它通过改进和修订进行。为了支持系统满足其需求的保证，最好在每个细化或修订步骤之后执行连续验证。为了实现实际应用，形式化系统建模和验证必须有效地支持持续验证。我们的建议，以解决这个问题是TOrPEDO，一种验证方法，模型通过部分Kripke结构（PKS）和要求指定为线性时间时序逻辑（LTL）属性。PKS支持细化，通过故意指示模型中稍后完成的未指定部分。我们支持两种互补形式的验证：通过模型检验和证明。模型检验可用于提供反例，即，查明违反需求的模型行为。相反，证明是有用的，因为它们可以解释为什么需求得到满足。在我们的工作中，我们引入了一个特定的概念证明，称为拓扑证明（TP）。一个TP产生一个切片的原始PKS证明财产满意度。因为模型可能是不完整的，所以TOrPEDO支持对需求满足、违反和可能满足的推理（在满足取决于未知部分的情况下）。
2018-11-26 cs.LO
Model Checking Data Flows in Concurrent Network Updates (Full Version)
我们提出了一个模型检验的方法来验证数据流的正确性，在网络配置的并发更新。该验证问题对于软件定义网络（SDN）非常重要，其中错误可能导致分组丢失、黑洞和安全违规。我们的方法是基于规范的时间属性的个人数据流，如要求流是免费的周期。我们检查这些属性是否同时满足所有活动的数据流，而网络配置更新。为了表示并发网络控制器的行为和由此产生的配置的演变，我们引入了一个扩展的Petri网的过境关系，其特征在于由Petri网的每个转变所引起的数据流。对于安全的Petri网与过境，我们减少了时间流属性的验证电路模型检验问题，可以解决有效的验证技术，如IC3，插值，有界模型检验。我们报告令人鼓舞的实验与原型实现的基础上的硬件模型检查ABC。
2019-11-14 cs.LO
Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking
网络中领导者的选举是一项具有挑战性的任务，特别是当进程是异步的时，即，执行具有时变周期的算法。Thales开发了一种工业选举算法，具有任意数量的过程，可能会失败。在这项工作中，我们证明了这种工业算法的一个变体的正确性。我们使用的方法相结合的抽象，SafeProver求解器，和参数定时模型检查。这使我们能够证明算法的正确性为大量的p进程（p=5000）。
2018-12-21 cs.LO
A benchmark library for parametric timed model checking
涉及硬时序约束和并发的实时系统的验证是至关重要的。参数定时模型检验允许在存在未知定时常数或不确定性（例如，周期的不精确性）的情况下进行形式化验证。随着近年来一些技术和工具的发展，以提高效率的参数化定时模型检验，有一个适当的基准测试和比较这些工具的需求越来越大。我们在这里提出了一个基准库参数定时模型检验的基准积累了多年。我们的基准包括学术基准，工业案例研究和使用现有技术无法解决的例子。
2018-12-20 cs.LO
Improving BDD Based Symbolic Model Checking with Isomorphism Exploiting Transition Relations
基于BDD的符号化模型检验大大提高了模型检验的适用性。然而，基于BDD的符号模型检验仍然非常消耗内存和时间。一个主要原因是系统之间复杂的过渡关系。有时，由于其穷举存储要求，甚至不可能生成转换关系。为了减少这个问题，已经提出了使用分区的过渡关系。然而，仍然有一些系统根本无法验证。此外，如果分区的粒度太细，则验证所需的时间可能增加。在本文中，我们的目标是异步并发系统的符号验证。对于这样的系统，我们提出了一种方法，它使用的相似性的过渡关系，以获得进一步的内存减少和运行时的改善。通过应用我们的方法，即使是以前棘手的过渡关系的系统的验证变得可行。
2011-06-07 cs.LO
Model Checking Techniques for Verification of an Encryption Scheme for Wireless Sensor Networks
在本文中，我们处理的形式化验证的加密方案的无线传感器网络（WSNs）。特别是，我们提出了我们的第一个结果，建立一个框架，致力于建模和验证的无线传感器网络方面。为了实现我们的目标，我们建议指定的WSNs模型编写的Petri网使用Promela结构，以验证它们的正确性属性，使用SPIN模型检查。我们首先指定在Promela的Petri网描述的无线传感器网络的加密方案，描述其行为。然后，正确性的属性，表达对系统的行为的要求，制定在线性时序逻辑（LTL）。最后，SPIN模型检查器用于检查模型是否具有特定的正确性属性，如果没有，则提供一个反例：不满足此属性的计算。这个反例将有助于发现最终问题的根源并加以纠正。
2013-05-18 cs.LO
Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
本文针对可实例化于多类车站的通用联锁逻辑，结合 Dafny 编码、模板不变式与参数化模型检验器生成的不变式，实现关键安全性质的自动化参数化验证。
2024-02-29 cs.LO
AutoHyper: Explicit-State Model Checking for HyperLTL
HyperLTL是一种可以表达超属性的时态逻辑，即，与系统的多个执行跟踪相关的属性。这样的性质变得越来越重要并且自然发生，例如，在信息流控制，鲁棒性，突变测试，路径规划和因果关系检查。到目前为止，HyperLTL的完整模型检验工具仅限于无替代公式，即，仅使用泛量化或仅使用存在迹量化的公式。涉及量词替换的属性只能以不完整的方式处理，即，即使该属性保持，验证也可能失败。在本文中，我们提出了AutoHyper，一个显式状态自动机为基础的模型检查器，支持完整的HyperLTL，并完成与任意量词交替的属性。我们表明，语言包含检查可以集成到HyperLTL验证，这使得AutoHyper受益于一系列现有的包含检查工具。我们评估AutoHyper的一组广泛的基准来自不同领域的文献，并将其与现有的（不完整的）方法进行HyperLTL验证。
2023-01-26 cs.LO
Lightweight Monte Carlo Verification of Markov Decision Processes with Rewards
马尔可夫决策过程是并发优化问题的有用模型，但对于穷举验证方法来说往往是棘手的。最近的工作已经引入了轻量级的近似技术，直接从调度空间采样，带来了可扩展的替代标准的数值模型检验算法的前景。到目前为止，重点一直是优化一个属性的概率，但许多问题需要定量分析的回报。因此，在这项工作中，我们提出了轻量级的统计模型检验算法，以优化马尔可夫决策过程的奖励。我们认为标准的定义中使用的奖励模型检验，引入一个辅助的假设检验，以适应可达性奖励。我们证明了我们的方法在一些标准的案例研究的性能。
2015-03-23 cs.LO
Automatic Verification of Timed Concurrent Constraint Programs
时间并发约束（Timed Concurrent Constraint，tccp）是并发约束编程（Concurrent Constraint Programming，cc）范式的扩展，它允许我们指定时间至关重要的并发系统，例如反应式系统。可以有无限多个状态的系统可以在tccp中指定。模型检验是一种能够自动验证具有大量状态的有限状态系统的技术。在过去的几年里，一些研究已经调查了如何扩展模型检验技术的系统具有无限数量的状态。在本文中，我们提出了一种方法，利用tccp的计算模型。基于约束的计算允许我们定义一种方法，将模型检验算法应用于（一类）无限状态系统。我们扩展的经典算法的模型检验LTL的一个特定的逻辑定义的验证tccp和tccp结构，我们在这项工作中定义的建模程序的行为。我们定义了一个限制的时间，以得到一个有限的模型，然后我们开发了一些说明性的例子。据我们所知，这是第一个为tccp定义模型检验方法的方法。
2005-05-11 cs.LO
Dynamic Verification of SystemC with Statistical Model Checking
许多嵌入式和实时系统具有固有的概率行为（传感器数据，不可靠的硬件等）。在这种情况下，至关重要的是评估系统属性，如“特定硬件故障的概率”。这样的属性可以通过使用概率模型检验来评估。然而，由于状态空间爆炸，这种技术在代表现实嵌入式和实时系统的模型上失败了。为了克服这个问题，我们提出了一个基于统计模型检验的验证框架。我们的框架是能够评估的概率和时间属性在SystemC，一个标准的系统级建模语言建模的大型系统。它作为Plasma-lab统计模型检查器的扩展完全实现。我们说明了我们的方法上的多升系统的案例研究。
2015-09-21 cs.LO cs.SE
SCTL: Towards Combining Model Checking and Proof Checking
模型检验和自动定理证明是形式化方法的两大支柱。本文从自动定理证明的角度研究模型检验，旨在将自动定理证明的表达性和模型检验的完全自动性结合起来。本文的重点是Kripke模型的时序逻辑性质的验证。本文的主要贡献是：首先定义了一个允许多元谓词符号的扩展计算树逻辑，然后以Kripke模型为参数，为该逻辑设计了一个证明系统，然后设计了一个用于该演算的证明搜索算法和一个新的自动定理证明器来实现它。验证过程是完全自动的，并且在属性不成立时产生一个反例，或者证书实验结果比较以及现有的国家的最先进的工具，在一些基准，包括应用到空中交通管制和设计选择，导致这种效率进行了讨论。
2017-09-30 cs.LO
Rewrite based Verification of XML Updates
我们考虑XML文档更新的访问控制问题。在XML编程的上下文中，类型可以被视为对冲自动机，静态类型检查相当于验证程序总是将有效的源文档转换为有效的输出文档。给定一组更新操作，我们特别感兴趣的是检查安全属性，例如在任何更新序列中保存文档类型。我们还感兴趣的相关政策的一致性问题，即检测是否授权的操作序列可以模拟禁止的。我们减少这些问题的类型检查问题，解决了计算变种的对冲自动机特征的祖先和后代的初始文档类型的参数化重写规则关闭。
2009-07-29 cs.LO
Model Checking Resource Bounded Systems with Shared Resources via Alternating Büchi Pushdown Systems
资源受限的多智能体系统的验证一般是不可判定的。在许多这样的设置中，资源对于代理是私有的。本文研究了基于交替时序逻辑（ATL）的资源逻辑在共享资源下的模型检验问题。资源可以被消耗和生产到任何数量。我们表明，模型检验问题是不可判定的，如果两个或两个以上的这样的无界资源。我们的主要技术成果是，在一个单一的共享资源的情况下，问题变得可判定。虽然直观，可判定性的证明是不平凡的。我们减少模型检验的问题交替Büchi下推系统。一个中间结果连接到一般的基于自动机的验证：我们表明，模型检验计算树逻辑（CTL）（紧凑）交替Büchi下推系统是可判定的。
2015-08-14 cs.LO
Stateless and Rule-Based Verification For Compliance Checking Applications
Sharif University of Technology（谢里夫理工大学）；University of California, Berkeley（加州大学伯克利分校）；Volkswagen Group Data:Lab（大众汽车集团数据实验室）
基础计算模型在任何计算中都有重要的作用。状态和变迁（如在自动机中）与规则和值（如在Lisp和逻辑程序设计中）是两个可比较和对应的计算模型。演绎和模型检验验证技术都依赖于状态的概念，因此，它们的底层计算模型是状态相关的。一些核查问题（如根据某些条例和规则核查不遵守制度的遵守情况检查）没有很强的状态或过渡概念。代表它，这些系统有一个强大的概念，价值符号和声明性规则定义在他们身上。SARV（无状态和基于规则的验证）是一个验证框架，旨在简化无状态和基于规则的验证问题（例如合规性检查）的整个验证过程。本文提出了一种基于形式逻辑的智能合规性检查系统框架。我们定义并介绍了这个框架，报告了一个案例研究，并给出了实验结果。案例研究是关于智能城市的协议合规性检查。使用此解决方案，可以对救援场景用例及其遵从性检查进行概述和建模。介绍了SARV的自动化引擎和合规性解决方案。基于300个数据实验，基于SARV的合规性解决方案在3125个记录的软件质量数据集上优于著名的机器学习方法。
2022-04-28 cs.AI cs.LO cs.SE
TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets
本文提出了一种针对Petri网的HyperLTL模型检查器，用于验证超属性，该工具集成于TAPAAL框架并展示了其在计算机网络领域的应用性能。
2026-01-09 cs.LO
From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
我们提出了一个有界等价性验证技术的高阶程序与局部状态。该技术结合了完全抽象的符号环境互模拟类似的符号游戏语义，新的技术，轻量级的状态不变的注释。这产生了没有假阳性或假阴性的等效性验证技术。该技术是有界完备的，因为所有的不等式都是自动检测到足够大的界限。此外，几个硬等价证明自动或后被注释与状态不变量。我们在一个名为Hobbit的工具原型中实现了该技术，并使用一组广泛的新的和现有的示例对其进行基准测试。霍比特人可以证明许多经典的等价关系，包括所有迈耶和西伯的例子。
2021-10-22 cs.LO cs.PL
Model Checking for Verification of Quantum Circuits
在这次演讲中，我们将描述一个基于断言的验证（ABV）的量子线路的框架，通过应用我们以前的工作中开发的量子系统的模型检查技术，其中：（i）无噪声和有噪声的量子线路分别建模为算子和超算子值的过渡系统，这两者都可以进一步表示为张量网络。(ii)量子断言由Birkhoff-von Neumann量子逻辑的时间扩展指定。它们的语义定义的基础上的设计决策：它们将被用于验证的量子线路的模拟经典计算机或人类推理，而不是量子物理实验（例如，测试通过测量）;（iii）可达性分析和模型检查的量子线路的算法开发的基础上收缩张量网络。我们观察到，许多优化技术计算关系产品中使用的BDD为基础的模型检测算法可以概括为收缩张量网络的量子线路。
2021-04-23 cs.AR cs.LO quant-ph
Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification
灯塔项目，如CompCert，seL 4，IronFleet和DeepSpec已经证明，通过在抽象系统规范和可执行实现之间建立细化关系，可以对整个系统进行全面验证。然而，现有的方法施加严重的限制，无论是抽象的系统规范，由于其有限的表现力或多功能性，或可执行代码，由于其依赖于次优的代码提取或无表现力的程序逻辑。我们提出了一种新的方法，结合了组成细化的抽象，基于事件的模型的分布式系统与验证的成熟的程序代码，使用表达分离逻辑，支持功能的现实程序设计语言，如可变堆数据结构和并发。我们的工作的主要技术贡献是一个正式的框架，健全的基于事件的系统模型，程序规范的分离逻辑，这样的成功验证建立了一个细化模型和代码之间的关系。我们在Isabelle/HOL中正式定义了我们的框架Igloo。我们的框架，使现有的程序验证器的协议开发工具的良好组合。我们报告的三个案例研究，领导人选举协议，复制协议，和安全协议，我们完善正式的要求到程序规范（在伊莎贝尔/HOL），我们在Java和Python中实现，并证明正确使用VeriFast和Nagini工具。
2020-10-09 cs.LO
Towards the Combination of Model Checking and Runtime Verification on Multi-Agent Systems
针对多智能体系统形式化验证难、模型检测问题通常不可判定的问题，提出结合模型检测与运行时验证的方法，用模型检测器验证可判定片段子模型、运行时监控器验证其余部分，并实现技术验证了效果。
2022-04-19 cs.LO cs.MA
Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking
Faculty of Informatics West University Timi s oara Romania
本文提出一种基于TLA+轨迹检查的监控工具，可从Kubernetes审计日志推断行为并检测多租户等违规，将形式化推理融入实时Kubernetes环境以提升监控与正确性检查效果。
2026-09-28 cs.DC cs.LO
C-SHORe: Higher-Order Verification via Collapsible Pushdown System Saturation
高阶递归模式（HORS）作为高阶函数程序的一个有用的抽象，受到了广泛的关注，许多新的验证技术采用HORS模型检查作为其核心。我们给一个帐户的C-SHORe工具，这有助于正在进行的追求一个真正可扩展的模型检查HORS提供一个不同的，自动机理论的角度来看。C-SHORe实现了第一个实用的模型检查算法，该算法作用于下推自动机的泛化，与HORS等表达，称为可折叠下推系统（CPDS）。其核心是CPDS的向后饱和算法。此外，它能够使用从近似向前可达性分析中收集的信息来指导其向后搜索。此外，它使用了一种算法，修剪的CPDS模型检查之前，并提取反例的方法，在负的情况下。我们提供了C-SHORe与HORS最先进验证工具的最新比较。该工具和其他材料可从http://cshore.cs.rhul.ac.uk获得。
2018-09-17 cs.LO
A Proof System with Causal Labels (Part II): checking Counterfactual Fairness
本文扩展TNDPQ演算，通过为因果标签制定结构条件并检查评估稳健性，验证概率分类器的反事实公平性。
2025-10-25 cs.LO
An Overview of the HFL Model Checking Project
在这篇文章中，我们给出了一个概述我们的项目高阶程序验证的基础上HFL（高阶不动点逻辑）模型检验。在简要介绍HFL之后，我们解释了如何将其应用于程序验证，并总结了该项目的现状。
2021-09-10 cs.LO cs.PL
Model Checking of Boolean Process Models
在业务流程管理领域，用于业务流程控制流的正式模型已经设计了15年以上。哪些方法最适合验证这些模型？第一步是选择一种固定模型语义的形式语言。我们采用布尔系统的语言作为布尔过程模型的参考语言。布尔系统是有色Petri网的一个简单子类。它们的特征是低令牌来显式地建模状态，随后跳过激活和任意逻辑规则类型AND，XOR，OR等来建模控制流的拆分和连接。我们采用模型检验作为布尔系统的安全性和活性的验证方法。布尔系统的模型检验利用命题逻辑的基本理论，不需要模态算子。我们的验证建立在一个有限的完整前缀的某个T-系统附加到布尔系统。它将布尔系统的进程分裂为有限长度的基进程集。它们的行为转化为命题逻辑的公式。我们的验证任务包括检查这些公式的可满足性。此外，我们已经实现了我们的模型检验算法作为一个java程序。验证给定布尔系统所需的时间主要取决于初始令牌的数量。由于该算法必须解决某些SAT问题，因此不能期望多项式复杂度。最后，本文对一些被设计成事件驱动过程链的布尔过程模型进行了模型检验。
2011-05-03 cs.LO
Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification
本文通过为{log}语言定义类型系统并实现类型检查器，将类型检查与集合约束求解结合，提高了软件验证的自动化程度，并通过两个工业案例验证了其有效性。
2024-03-21 cs.LO cs.PL
Some approximations in Model Checking and Testing
模型检验和测试是两个具有相似目标的领域：验证系统是否满足属性。他们从系统的不同假设开始，并开发了许多具有不同近似概念的技术，当精确的验证可能在计算上太难时。本文介绍了近似的概念及其逻辑和统计背景，并由此引出了几种模型检验和测试技术：有界模型检验、近似模型检验、近似黑盒检验、近似基于模型的测试和近似概率模型检验。所有这些方法都保证了验证的质量和效率。
2013-04-16 cs.LO cs.SE
Leveraging Datapath Propagation in IC3 for Hardware Model Checking
针对 IC3 数据路径抽象产生冗余抽象状态空间的问题，提出利用具体常量迭代传播数据路径操作结果并生成引理以收紧抽象，实验表明其优于现有先进验证器。
2023-09-26 cs.LO
Checking Zenon Modulo Proofs in Dedukti
Dedukti被认为是一个通用的证明检查器。它是一个基于lambda Pi演算模的逻辑框架，用作后端来验证来自定理证明器的证明，特别是那些实现某种形式重写的证明。我们提出了一个浅嵌入到Dedukti的证明Zenon模，扩展表为基础的一阶定理证明Zenon演绎模和类型。Zenon Modulo适用于学术和工业项目中的程序验证。我们嵌入的目的是通过分离不可信的证据搜索和可信的证据验证来增加自动生成的证据的可信度。
2015-07-31 cs.LO
Regular Model Checking Revisited (Technical Report)
在这方面的贡献，我们重温定期模型检验，一个强大的框架，已成功地应用于验证的无限状态系统，特别是参数化系统（并发系统与任意数量的进程）。我们提供了一个重新制定的定期模型检验与长度保持传感器在存在的二阶理论在自动结构。我们认为，这是一个自然的配方，使我们能够利用强大的综合技术，已被广泛研究的软件验证社区。更确切地说，在这个公式中，一阶部分表示所需正确性属性的验证条件（我们有完整的求解器），而存在量化的二阶变量表示要合成的关系。我们表明，许多有趣的正确性可以用这种方式制定，例如安全，活性，双相似性，和游戏。更重要的是，我们表明，这种新的配方允许新的有趣的基准（和旧的定期模型检验基准，以前被认为是困难的），特别是在参数化系统验证领域，要解决。
2021-11-21 cs.FL cs.LO
A Practitioner's Guide to MDP Model Checking Algorithms
马尔可夫决策过程（MDP）的模型检验非折扣可达性和期望回报特性是验证不确定系统的关键。流行的算法是策略迭代和价值迭代的变体;在工具竞争中，大多数参与者都依赖后者。这些算法通常需要最坏情况下的指数时间。然而，这个问题同样可以用公式表示为线性规划，在多项式时间内可解。在本文中，我们给出了一个详细的概述，今天的国家的最先进的算法MDP模型检验的重点是性能和正确性。我们强调它们的根本区别，并描述各种优化和实施变体。我们实验比较浮点和精确算术实现的所有算法在三个基准集使用两个概率模型检查器。我们的研究结果表明，（乐观）值迭代是一个明智的默认值，但其他算法在特定的设置是更可取的。因此，本文为MDP验证实践者-工具构建者和用户提供了指南。
2023-01-24 cs.LO
SMT-based Verification of LTL Specifications with Integer Constraints and its Application to Runtime Checking of Service Substitutability
在基于服务的应用程序的执行过程中出现的一个重要问题涉及确定是否可以用具有不同接口的服务来替换正在运行的服务的能力，例如，如果前者不再可用。标准有界模型检验技术可用于执行此检查，但它们必须能够非常快速地提供答案，以免检查妨碍应用程序的可操作性，而不是帮助它。当考虑会话服务时，问题变得更加复杂，即，服务，公开其中具有输入/输出数据依赖关系的操作。在本文中，我们介绍了一个形式化验证技术的线性时序逻辑，允许用户在公式中的整数变量的约束的扩展。这种技术适用于会话服务的可替代性问题被证明是相当快，比现有的内存占用更小。
2010-04-16 cs.LO cs.SE
Equivalence Checking in Embedded Systems Design Verification
在这份报告中，我们专注于嵌入式系统的建模和形式化验证相关的一些方面。已经提出了许多模型来表示嵌入式系统。这些模型涵盖了广泛的风格，特点和应用领域，包括有限状态机，数据流图，通信过程和Petri网的扩展。在本报告中，我们使用了PRES+模型（基于Petri网的嵌入式系统表示）作为经典Petri网模型的扩展，该模型捕获了嵌入式系统的并发性和时序行为;它允许系统在不同的抽象级别中具有代表性，并通过允许令牌携带信息来提高表达能力。如上所述，使用PRES+建模可能便于指定输入行为，因为它支持并发性。然而，据我们所知，文献中没有报道PRES+模型的等价性检查方法。相反，存在FSMD模型的等价性检查。作为第一步，因此，我们试图设计一个算法，将PRES+模型FSMD模型。
2010-08-20 cs.FL cs.LO
Quantitative Model Checking of Linear-Time Properties Based on Generalized Possibility Measures
基于可能性测度的线性时间特性的模型检验在以前的工作（Y。Li和L. Li，模型检验基于可能性度量的线性时间特性，IEEE Transactions on Fuzzy Systems，21（5）（2013），842-854）。然而，在以前的工作中考虑的线性时间性质是经典的和定性的，系统的可能性信息没有考虑在所有。本文将研究基于广义可能性测度的模糊线性时间性质的定量模型检验。使用可能性信息来描述系统的模型以及系统需要遵守的属性，以识别模型/属性中的不确定性。系统采用{ \sl广义可能性Kripke结构}（GPKS，简称）建模，其性质用模糊线性时间性质描述.具体地，研究了GPKS系统的可达性、总是可达性、约束可达性、重复可达性和持续性的模糊线性时间性质。介绍了GPKS中的模糊正则安全性质和模糊$ω-$正则性质，深入研究了模糊有限自动机对模糊正则安全性质和模糊$ω-$正则性质的验证.证明了有限GPKS中模糊正则安全性和模糊$ω-$正则性的验证可以转化为本文所介绍的产品GPKS中（总是）可达性和重复可达性（持久性）的验证.文中给出了几个算例来说明本文所提出的方法。
2016-01-25 cs.LO
Verifying Reachability Properties in Markov Chains via Incremental Induction
在概率验证和非概率验证之间存在可扩展性差距。概率模型检验工具基于显式引擎或（多端）二元决策图。这些结构在非概率验证领域得到了更可扩展的技术（如IC3）的补充。我们提出了一个符号概率模型检验算法的基础上IC3类增量建设的归纳条款划分的状态空间，交错与增量建设的线性不等式系统。本文比较了我们的实现标准的定量验证的替代方案：我们的实验表明，我们的算法是一个步骤，以更可扩展的符号验证有限状态马尔可夫链中的罕见事件。
2019-09-19 cs.LO
Verification of Peterson's Algorithm for Leader Election in a Unidirectional Asynchronous Ring Using NuSMV
大多数分布式算法的有限内在本质使我们能够使用模型检验工具来验证这类算法。在本文中，我试图使用NuSMV作为一个模型检验工具，验证必要的性质彼得森的领导选举问题的单向异步环形拓扑结构的算法。Peterson的异步环算法假设环中的每个节点都有一个唯一的ID和一个用于处理存储问题的队列。考虑到队列可以有任何值的组合，一个只有四个节点的环的构造模型将有超过十亿个状态。虽然似乎模型检验是不是一个可行的方法，这个问题，我试图使用几个有效的限制性假设雇用正式的模型检验的方法，而不会失去正确的功能的彼得森算法。这些强制限制假设的目标是模型检验过程中的自由度，并显着减少CPU时间，内存使用和页面错误的总数。通过部署这些限制，在NuSMV的模型检验过程中，节点数量可以从4个增加到8个。
2008-08-07 cs.DC cs.LO
Proceedings First Workshop on Pre- and Post-Deployment Verification Techniques
PrePost（部署前和部署后验证技术）研讨会旨在汇集计算机辅助验证和验证领域的研究人员，讨论部署前和部署后验证技术之间的联系和相互作用。研讨会涵盖的主题的例子是经典的模型检验和测试之间的关系，一方面和运行时验证和统计模型检验另一方面，类型系统之间的关系，可以通过静态或动态检查技术，如运行时监控。
2016-05-25 cs.LO cs.SE
Multi-Agent Verification and Control with Probabilistic Model Checking
University of Oxford（牛津大学）
本文综述了概率模型检验与博弈论结合以验证多智能体交互的进展，并探讨其在人工智能、机器人等领域的应用及未来挑战。
2023-08-05 cs.AI cs.LO
Real-Time Model Checking Support for AADL
我们描述了一个模型检查工具链的AADL模型的行为验证，考虑到语言的实时语义，这是兼容的AADL行为附件。我们给出了一个高层次的视图的工具和转换中涉及的验证过程，并专注于我们的框架检查用户定义的属性提供的支持。我们还描述了在一个重要的航空电子演示器上获得的实验结果，该演示器模拟了负责飞机和地面站之间数据通信的网络协议。
2015-03-02 cs.LO cs.SE
Equivalence Checking in Embedded Systems Design Verification using PRES+ model
本文主要研究嵌入式系统的建模和形式化验证。已经提出了许多模型来表示嵌入式系统。这些模型涵盖了广泛的风格，特点和应用领域，包括有限状态机，数据流图，通信过程和Petri网的扩展。在本报告中，我们使用了PRES+模型（基于Petri网的嵌入式系统表示）作为经典Petri网模型的扩展，该模型捕获了嵌入式系统的并发性和时序行为;它允许系统在不同的抽象级别中具有代表性，并通过允许令牌携带信息来提高表达能力。如上所述，使用PRES+建模可能便于指定输入行为，因为它支持并发性。然而，据我们所知，文献中没有报道PRES+模型的等价性检查方法。相反，存在FSMD模型的等价性检查。因此，作为第一步，我们寻求设计一种算法来将PRES+模型转换为FSMD模型，并且我们寻求在现实生活中的示例上手动执行我们的算法，并且我们必须将两个版本的PRES+模型转换为FSMD模型。然后使用现有的等价性检查器，我们已经检查了两个FSMD模型之间的等价性。
2010-10-24 cs.FL cs.LO
Foundations for Entailment Checking in Quantitative Separation Logic (extended version)
定量分离逻辑（QSL）是分离逻辑（SL）的扩展，用于概率指针程序的验证。在QSL中，公式计算为实数而不是真值，例如，在给定的符号堆中，内存安全终止的概率。与\SL一样，使用QSL进行推理时的一个关键问题是\emph{entailment}：公式f是否包含另一个公式g？我们给出了从QSL中的蕴涵检查到SL中的蕴涵检查的一般性约简。这允许利用大量的SL研究来自动验证概率指针程序。我们分析了我们的方法的复杂性，并证明其适用性。特别是，我们得到的第一个可判定性结果，验证这些程序通过应用我们的减少到一个量化的扩展著名的符号堆片段的分离逻辑。
2022-01-27 cs.LO cs.PL
Platform Dependent Verification: On Engineering Verification Tools for 21st Century
本文综述了与平台相关的显式状态LTL模型检验的最新进展。
2011-11-02 cs.LO cs.SE
Distributed CTL Model Checking in the Cloud
最近广泛使用的“大数据”平台要求形式化验证社区更广泛地采用。事实上，形式化验证需要高性能的数据处理软件，用于从来自被分析系统的空前数量的数据中提取知识。由于基于云的计算资源已经变得易于访问，因此验证技术和工具有机会经历深刻的技术转型，以利用新的可用架构。这使得人们对并行化和分布式验证技术越来越感兴趣。在本文中，我们介绍了一种分布式的方法，利用通常使用的技术，由“大数据”社区，使验证的计算树逻辑（CTL）公式非常大的状态空间，使用分布式系统和云计算设施。基准规范上进行的几个测试的结果，从而显示所提出的方法的方便。
2013-10-24 cs.DC cs.LO cs.SE
Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms
我们介绍了一种用于容错分布式算法（FTDA）的自动参数化验证方法。FTDA由进程数和假定的拜占庭故障进程的最大数目参数化。在我们的技术的中心是一个参数区间抽象（PIA）的区间边界是参数的算术表达式。使用PIA的数据抽象和一种新形式的计数器抽象，我们减少了参数化的问题，有限状态模型检验。我们证明了我们的方法的实际可行性，通过验证Srikanth和Toueg著名的分布式算法的几个变种。我们的半决策程序的补充和动机的不可判定性证明FTDA验证，即使在没有进程间通信。据我们所知，这是第一篇实现拜占庭FTDA参数化自动验证的论文。
2013-02-03 cs.DC cs.LO
Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement
LMU Munich（慕尼黑大学）
本文提出了一种基于并行轨迹抽象细化的多线程软件模型检查方法，通过利用多核CPU提升验证效率，优于传统顺序方法和DSS技术。
2026-01-15 cs.LO cs.PL cs.SE
Model Checking Contractual Protocols
本文讨论了如何模型检验，用于验证动态系统的行为需求的技术，可以有效地部署合同的验证。对当事人之间的协议采取过程观点，即合同随着时间的推移在影响其状态变化的行为或更一般的事件方面的演变而被建模。建模是用Petri网在其他研究工作的贸易程序的代表性的精神。本文通过一个例子说明了验证技术的所有阶段，并认为这种方法是有用的，特别是在合同前谈判和合同起草的背景下。这里报告的工作是一个更广泛的项目的一部分，对基于逻辑的工具，用于分析和表示的法律合同的发展。
2001-06-07 cs.LO cs.SE
VeriPy Source-Preserving Verification and Compatibility Checking for Python Components
Astrio Labs（Astrio实验室）
VeriPy提出一种统一工作流，通过注释表达契约并生成Dafny/Lean工件，实现Python组件的源级验证与向后兼容性检查。
2026-10-05 cs.LO cs.PL cs.SE
Boost the Impact of Continuous Formal Verification in Industry
软件模型检验在过去的二十年里取得了长足的进步，但其可扩展性和适应性仍然是制约其实际应用的主要瓶颈之一。在这里，我们描述了一种通过利用持续集成和回归测试等实践将软件模型检验技术集成到DevOps文化中的方法。特别是，我们提出的方法着眼于修改的软件系统，因为它的最后一次验证，并提交给一个连续的形式化验证过程中，一组回归测试用例的指导下。我们的愿景是专注于开发人员，通过使用他们的主要软件开发方法和工具，将形式化验证技术集成到开发人员的工作流程中。
2019-07-17 cs.LO cs.SE
Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes free
Institut Supérieur de Gestion, Université de Tunis（突尼斯大学高等管理学院）
该研究指出机器检查使数学验证变得丰富但裁决稀缺，区分了验证的三个层次，通过测量成果集说明负担转移，并提出相关分类法、披露方案及应用启示。
2026-09-01 cs.AI cs.LO
Auto-Tuning High-Performance Programs Using Model Checking in Promela
本文提出利用模型检查中的反例加速高性能程序自动调优，以OpenCL程序为例，结合Promela和SPIN工具实现并验证了该方法。
2023-05-16 cs.DC cs.LO
Model-Checking of Linear-Time Properties in Multi-Valued Systems
本文研究多值系统线性时间性质的模型检验。介绍了多值逻辑系统的安全性、不变性、活性性、持久性和双持久性。讨论了与上述多值线性时间性质相关的一些算法。研究了利用格值自动机对多值正则安全性质和多值$ω$ -正则性质的验证。由于不矛盾定律（即，$a\wedge \neg a=0$）和排除中间法则（即，$a\vee \neg a=1$）在多值逻辑中不成立，本文引入的线性时间性质与经典逻辑中的线性时间性质相比有了新的形式。与经典的模型检验方法相比，本文提出的多值模型检验方法更加直观。本文还提出了一种新的带隶属度的多值模型检验方法。特别是，我们证明了多值模型检验可以简化为经典的模型检验。给出了相关的验证算法。文中还提供了一些说明性的例子和案例研究。
2016-09-25 cs.FL cs.LO
