Verifying Fixed-Point Digital Filters using SMT-Based Bounded Model Checking
在基于定点运算的处理器中实现数字滤波器会导致与有限字长相关的问题。特别地，在这样的滤波器中的信号的处理可以产生由在累加加法和乘法运算期间的量化和舍入效应引起的溢出和不想要的噪声。在本文中，我们描述了一种新的方法来验证数字滤波器使用现成的有界模型检查器称为ESBMC，它支持完整的C/C++，是基于可满足性模理论求解器。特别是，我们能够验证溢出的发生，极限环，和时间约束的基础上实现的离散时间模型在C。实验表明，该方法可以用来验证数字滤波器定点实现中的潜在问题，从而可以有效地发现现实的设计错误。
2013-07-23 cs.LO cs.SE
On verifying expectations and observations of intelligent agents
Indian Statistical Institute（印度统计研究所）；ENS Rennes（雷恩高等师范学院）
公共观察逻辑（Public Observation Logic，POL）是动态认知逻辑的一种变体，用于推理代理人的期望和代理人的观察。智能体对当前的情况有一定的期望，这些期望是由相关的协议驱动的，他们会排除期望与观察不匹配的可能世界。在这项工作中，我们调查的计算复杂性的模型检验问题的POL和证明其PSPACE-完全。我们还研究了POL的各种语法片段。我们验证了POL模型检验在验证交互式系统的不同特性和功能方面的不同期望和（匹配）观察系统的适用性。最后，我们对模型检验算法的实现进行了讨论。
2022-05-12 cs.AI cs.CC cs.LO
Verifying Isolation Properties in the Presence of Middleboxes
路由器转发表的正确性验证近年来取得了很大的进展。然而，这些方法不适用于包含诸如缓存和防火墙之类的中间盒的网络，这些中间盒的转发行为取决于先前观察到的流量。我们将探讨如何使用模型检验来验证包含此类“动态数据路径”元素的网络中的隔离属性。我们的工作利用了SMT求解器的最新进展，主要挑战在于扩展该方法以处理大型复杂网络。虽然模型检验在这个问题上的直接应用只能处理非常小的网络（如果有的话），但我们的方法可以在几分钟内在包含30，000个中间盒的网络上验证简单的现实不变量。
2014-09-26 cs.LO cs.NI
Verifying Reachability Properties in Markov Chains via Incremental Induction
在概率验证和非概率验证之间存在可扩展性差距。概率模型检验工具基于显式引擎或（多端）二元决策图。这些结构在非概率验证领域得到了更可扩展的技术（如IC3）的补充。我们提出了一个符号概率模型检验算法的基础上IC3类增量建设的归纳条款划分的状态空间，交错与增量建设的线性不等式系统。本文比较了我们的实现标准的定量验证的替代方案：我们的实验表明，我们的算法是一个步骤，以更可扩展的符号验证有限状态马尔可夫链中的罕见事件。
2019-09-19 cs.LO
The Complexity of Verifying Strategic Abilities in Succinct Multiagent Systems
Griffith University（格里菲斯大学）；CNRS, LIPN, Sorbonne Paris North University（法国国家科学研究中心，LIPN，索邦巴黎北大学）；University of Naples Federico II（那不勒斯费德里科二世大学）；University of New South Wales（新南威尔士大学）
本文研究不完全信息下多智能体系统策略能力验证的复杂性，证明SLK_P和SLK的简洁模型检验为AEXP(poly)完全，目标ATL和ATL*为P^{NEXP}完全，修正了相关旧结果并明确了主观语义下的复杂度性质。
2026-10-13 cs.LO
Verifying Verified Code
Chong等人最近在AWS的一个案例研究中提出了一种有效的工业界有界模型检验方法。在本文中，我们报告了一个后续的案例研究，从三个研究问题的角度探讨了方法：（a）证明工件可以跨验证工具使用;（b）验证代码中是否存在错误;（c）规范是否可以改进。为了研究这些问题，我们将$\texttt{aws-c-common}$库的验证任务移植到SEAHORN和KLEE。我们展示了使用编译器语义和交叉检查规范与不同的验证技术的好处，并呼吁标准化证明库扩展，以增加规范的重用。讨论的核查任务可在网上公开查阅。
2021-07-01 cs.LO cs.SE
Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains
本文针对量子连续时间马尔可夫链，提出结合代数与数值方法的连续随机逻辑模型检验方案，确立了CSL的可判定性并保证计算效率，还给出示例演示方法应用。
2025-11-10 cs.LO
Verifying Quantized Neural Networks using SMT-Based Model Checking
Federal University of Amazonas（亚马孙联邦大学）；University of Manchester（曼彻斯特大学）；TPV Technology（TPV技术公司）
人工神经网络（ANN）正被部署用于越来越多的安全关键型应用，包括自动驾驶汽车和医疗诊断。然而，由于其黑箱性质和对对抗攻击的明显脆弱性，人们对它们的可靠性提出了担忧。当人工神经网络部署在受限系统上时，这些问题被放大，这限制了数学运算的精度，从而引入了额外的量化误差。在这里，我们开发和评估一种新的符号验证框架，使用软件模型检验（SMC）和可满足性模理论（SMT）检查人工神经网络中的漏洞。更具体地说，我们提出了几个人工神经网络相关的优化SMC，包括通过区间分析，切片不变的推理，表达式简化，和离散化的非线性激活函数。有了这个验证框架，我们可以提供正式保证的安全行为的人工神经网络实现在浮点和定点运算。在这方面，我们的验证方法能够验证和产生对抗的例子，$52$测试用例跨越图像分类和一般的机器学习应用。此外，对于中小型ANN，我们的方法在几分钟内完成了大部分验证运行。此外，与大多数最先进的方法相比，我们的方法不限于关于激活函数和非量化表示的特定选择。我们的实验表明，我们的方法可以分析更大的ANN实现，并大大减少了验证时间相比，使用SMT解决的最先进的技术。
2021-09-16 cs.CR cs.LG cs.LO
Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report)
我们考虑的问题，自动验证一个参数化的概率并发系统的家庭终止的概率为1的所有实例对抗对抗的竞争对手。一个参数化的族定义了一个无限状态系统：对于每个数n，这个族由一个实例和n个有限状态进程组成。与安全性相比，活性的参数化验证目前仍然被认为是极具挑战性的，特别是在模型中存在概率的情况下。一个主要的挑战是提供一个足够强大的象征性框架。一个著名的符号框架的参数化验证的非概率并发系统是定期模型检验。虽然该框架最近扩展到概率系统，将公平性的框架-通常是至关重要的验证终止-一直特别困难，由于存在无限数量的公平性约束（每个过程一个）。我们的主要贡献是一个系统的，正则保持，编码有限的公平性（一个现实的公平性的概念，提出了由Henzinger）定期模型检验的概率参数化系统的框架。我们的编码减少了终止有限的公平性，以验证参数化的终止没有公平性的概率系统在定期模型检验（验证框架已经存在）。我们表明，我们的算法可以验证终止许多有趣的例子，从分布式算法（赫尔曼的协议）和进化生物学（莫兰过程，细胞周期开关），这并不符合标准的公平概念。据我们所知，我们的算法是第一个全自动的方法，可以证明这些例子的终止。
2017-10-30 cs.DC cs.FL cs.LO
Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)
RPTU University Kaiserslautern-Landau（莱茵兰-普法尔茨技术大学凯泽斯劳滕-兰道分校）；Max Planck Institute for Software Systems (MPI-SWS)（马克斯·普朗克软件系统研究所）
REAL工具通过高效消除Ramsey量词，在LIRA中实现快速消除，应用于存活性检查和单子分解等程序验证问题。
2026-01-22 cs.FL cs.LO
Learning Representations Through Contrastive Neural Model Checking
CISPA Helmholtz Center for Information Security（CISPA 欧洲信息安全研究中心）
该研究针对形式化验证领域表示学习探索不足的问题，提出对比神经模型检验CNML方法，通过自监督对比目标将逻辑规范与系统嵌入共享潜在空间，在检索任务上表现优于基线且可迁移泛化，为形式化语言表示学习提供了新目标。
2025-10-03 cs.LG cs.LO
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
Marimba: A Tool for Verifying Properties of Hidden Markov Models
Instituto de Investigaciones en Matemáticas Aplicadas y en Sistemas（应用数学与系统研究所）；University of Bristol（布里斯托尔大学）；Bristol Robotics Laboratory（布里斯托尔机器人实验室）；Universidad Nacional Autónoma de México（墨西哥国立自治大学）
对隐马尔可夫模型（Hidden Markov Models，简称HMM）的性质进行形式化验证，对于保证模型和系统的正确性具有重要意义。HMM验证的一个重要步骤是Zhang等人开发了一系列用于验证HMM的逻辑，称为POCTL* 及其模型检验算法。据我们所知，我们在这里介绍的验证工具是第一个基于张等人。的方法。作为其有效的应用程序的一个例子，我们验证了在人机交互的上下文中的移交任务的属性。我们的工具在Haskell中实现，并使用人形机器人Bert 2进行实验评估。
2015-10-28 cs.LO cs.RO
Parameterized Verification of Quantum Circuits (Technical Report)
本文提出了一种自动框架用于验证参数化量子电路的输入输出正确性与等价性，采用同步加权树自动机模型并提供决策算法，通过实验展示了框架的高效性与表达力。
2025-12-02 cs.FL cs.LO
Generating Counterexamples for Model Checking by Transformation
反例解释了为什么所需的时间逻辑属性无法保持。反例的产生被认为是模型检验作为一种验证技术的主要优点之一。此外，当模型检验确实成功地验证了属性时，通常不存在可用作已验证属性的证据的独立可检验见证。在此之前，我们已经展示了程序转换技术如何用于验证反应系统的安全性和活性特性。然而，没有反例或证人使用所描述的技术产生。在本文中，我们将讨论这个问题。特别是，我们展示了如何程序转换技术蒸馏可以用来促进反应系统的时间属性的反例和证人的建设。示例系统的目的是相互排斥模型进行分析，使用这些技术的安全性（相互排斥）和活性（非饥饿），与反例生成的那些属性不举行。
2016-07-08 cs.LO cs.SE
Towards the Combination of Model Checking and Runtime Verification on Multi-Agent Systems
针对多智能体系统形式化验证难、模型检测问题通常不可判定的问题，提出结合模型检测与运行时验证的方法，用模型检测器验证可判定片段子模型、运行时监控器验证其余部分，并实现技术验证了效果。
2022-04-19 cs.LO cs.MA
Verifying Digital Systems with MATLAB
Federal University of Amazonas（亚马孙联邦大学）；University of Oxford（牛津大学）；Samsung Electronics（三星电子）
本文提出一个MATLAB工具箱，用于检查固定点数字系统中常见的设计错误，如溢出、限环、量化、稳定性和最小相位误差，适用于转移函数和状态空间方程表示的数字系统。
2017-02-18 cs.LO cs.SY eess.SY
Developing a Numerical Algorithm with CIVL Model Checking in the Loop
Argonne National Laboratory（阿贡国家实验室）；RIKEN Center for Computational Science（理化学研究所计算科学中心）
本研究在Flash-X框架中开发CIC沉积算法，通过提取接口至小C模型并用CIVL模型检查器验证物理性质、内存安全及并发性，发现随机测试遗漏的缺陷，提高了算法可靠性。
2026-09-29 cs.LO physics.comp-ph
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
Probabilistic Model--Checking of Quantum Protocols
我们建立了量子协议形式化验证的基本和通用技术。量子协议是一种新型的通信方案，涉及使用量子力学现象来表示、存储和传输数据。与量子计算机相反，量子通信系统可以并且已经使用当今技术实现;因此，严格建模和分析此类系统的能力至关重要。虽然目前对量子协议的分析使用传统的数学方法，并且需要对底层物理学有相当多的了解，但我们认为自动验证技术提供了一种优雅的替代方案。我们通过使用PRISM（一种概率模型检查工具）来演示这些技术。我们的方法在概念上比现有的证明简单，并允许我们消除协议定义的歧义，并评估其属性。它还有助于对实际执行的系统进行详细分析。我们说明了我们的技术建模选择的量子协议（即超密集编码，量子隐形传态，和量子纠错），并验证其基本的正确性。我们的研究结果为进一步建模和分析更大的系统（例如用于量子密码学的系统）提供了基础，其中基本协议被用作组件。
2005-10-05 cs.LO quant-ph
Incremental Symbolic Bounded Model Checking of Software Using Interval Methods via Contractors
有界模型检验（BMC）对于发现程序属性冲突至关重要。对于不安全的程序，BMC可以快速找到从初始状态到违反状态的执行路径，从而反驳给定的安全属性。然而，BMC技术难以伪造包含循环的程序。BMC需要将程序循环逐步展开到绑定$k$，从而暴露属性冲突，这可能导致探索相当大的状态空间。在这里，我们描述和评估的第一个验证方法的基础上，通过承包商的区间方法，以减少域的变量表示的搜索空间。这种减少是基于建模为代表承包商约束的函数的指定属性。特别是，我们利用区间方法通过承包商增量分析程序循环变量和合同的属性保证举行修剪搜索探索的域，从而减少资源消耗积极。实验结果表明，我们所提出的方法的效率和有效性在一个大的基准集，包括$7044$验证任务，与国家的最先进的BMC工具相比。我们提出的方法可以减少内存使用高达$75$ \%，而验证$1$ \%更多的验证任务。
2022-09-21 cs.LO cs.SE
Efficient Parallel Statistical Model Checking of Biochemical Networks
我们考虑的问题，验证生化网络的随机模型对时间逻辑术语表示的行为特性。精确的概率验证方法，例如CSL/PCTL模型检验，被巨大的计算需求所破坏，这使得它们被排除在大多数真实案例研究之外。要求较低的方法，如统计模型检验，通过从随机模型中抽样执行来估计满足属性的可能性。我们提出了一种方法，有效地估计的可能性，LTL属性P持有的随机模型的生化网络。与其他统计验证技术一样，我们提出的方法使用随机模拟算法来生成执行样本，但是有三个关键方面可以提高效率：首先，样本生成是由P的动态验证驱动的，这导致了最佳的整体模拟时间。其次，P保持概率的置信区间估计基于威尔逊方法的有效变体，可确保更快的收敛。第三，整个方法的设计，根据一个并行的方式和原型软件工具已经实施，并行执行采样/验证过程中的HPC架构。
2009-12-13 cs.CE cs.DC cs.LO
