Computation of Feasible Assume-Guarantee Contracts: A Resilience-based Approach
Newcastle University（纽卡斯尔大学）；University Mohammed IV Polytechnic (UM6P)（穆罕默德四世理工大学）；University of Birmingham（伯明翰大学）
本文提出了一种基于鲁棒性的方法，用于计算互联离散时间系统中满足时间规范的可行假设-保证合同，并通过实例展示了该方法在验证时序逻辑规范中的应用。
2025-12-08 cs.LO cs.SY eess.SY
Re-verification of a Lip Synchronization Protocol using Robust Reachability
时间自动机是描述和分析实时系统的重要模型。鲁棒性是在时钟出现小漂移或测试防护装置不精确的情况下模型的正确性。实现了一种分析时间自动机鲁棒性的符号算法。在本文中，我们重新分析了一个工业案例唇同步协议使用新的鲁棒可达性算法。这个唇同步协议是一个有趣的情况下，因为定时方面是至关重要的协议的正确性。该模型的几个版本被认为是：一个理想的视频流，锚定抖动，和非锚定抖动。
2010-03-01 cs.LO
Simulating reachability using first-order logic with applications to verification of linked data structures
本文介绍了如何利用现有的一阶逻辑定理证明器自动验证执行动态存储分配和破坏性更新的指针值结构字段的命令式程序的安全属性。其中一个主要的障碍是指定和证明（缺乏）的可达性动态分配的细胞之间的属性。主要的技术贡献是使用一阶公式以保守的方式模拟可达性的方法-该公式描述了一组程序状态的超集，如果有一个精确的方式来表达可达性，则会指定该超集。这些方法用于半自动程序验证（即，使用程序员提供的循环不变量），例如标记并清除垃圾回收和单链表的破坏性反转。(The标记和扫描的例子以前已经被报道为超出了ESC/Java的能力。
2009-05-27 cs.LO cs.PL
The Cost of Parameterized Reachability in Mobile Ad Hoc Networks
我们调查的影响，自发运动的复杂性验证问题的自动机为基础的协议模型的网络与选择性广播通信。我们首先考虑错误状态的可达性，并证明参数化验证是可判定的多项式复杂性。然后，我们转向更丰富的查询，并显示当考虑具有否定或基数约束的属性时，复杂性如何变化。
2012-02-27 cs.LO
Pushdown Timed Automata: a Binary Reachability Characterization and Safety Verification
我们认为下推时间自动机（PTA）的时间自动机（密集的时钟）增加了下推堆栈。PTA的配置包括控制状态、密集时钟值和堆栈字。通过使用模式技术，我们给出了二进制可达性的可判定特征（即，PTA的所有配置对的集合，使得一个可以到达另一个）。由于一个时间自动机可以被视为一个PTA没有下推栈，我们可以证明，二进制可达性的时间自动机是定义在实数和整数的加法理论。结果可用于验证稠密变量和无界离散变量上均包含线性关系的一类性质。这些性质以前不能用经典的区域技术来验证，也不能用时间自动机的时间时序逻辑和下推系统的CTL $^*$来表示。这些结果也被推广到时间自动机的其他推广。
2001-10-02 cs.LO
Verifying Reachability Properties in Markov Chains via Incremental Induction
在概率验证和非概率验证之间存在可扩展性差距。概率模型检验工具基于显式引擎或（多端）二元决策图。这些结构在非概率验证领域得到了更可扩展的技术（如IC3）的补充。我们提出了一个符号概率模型检验算法的基础上IC3类增量建设的归纳条款划分的状态空间，交错与增量建设的线性不等式系统。本文比较了我们的实现标准的定量验证的替代方案：我们的实验表明，我们的算法是一个步骤，以更可扩展的符号验证有限状态马尔可夫链中的罕见事件。
2019-09-19 cs.LO
Safety Verification of Stochastic Systems under Signal Temporal Logic Specifications
研究随机系统在信号时序逻辑规范下的验证问题，提出STL侵蚀策略，将概率验证转化为更严格的确定性验证，可与现有算法无缝集成，数值实验验证了其有效性。
2025-02-11 cs.FL cs.LO cs.SY
Fixed Point Certificates for Reachability and Expected Rewards in MDPs
本文提出基于初等不动点理论的证书，用于马尔可夫决策过程的可达性与期望奖励模型检查，并在Isabelle/HOL中形式化验证，增强Storm模型检查器生成证书，实现基准集的首次正式认证。
2025-01-20 cs.DM cs.LO cs.SY
Verification of Switched Stochastic Systems via Barrier Certificates
提出了一种连续时间切换随机系统的时序逻辑验证方法。我们的目标是找到一个复杂的时间属性满足在有限的时间范围内的概率的下限。所需的时间属性的系统表示使用一个片段的线性时序逻辑，称为安全的LTL相对于有限的痕迹。我们的方法结合了基于自动机的验证和屏障证书的使用。它依赖于分解的自动机与规范的否定成一系列更简单的可达性任务和计算这些可达性概率的上限，通过共同的或多个障碍证书。通过应用反例引导归纳合成框架来寻找障碍证书，说明了理论结果。
2021-09-25 cs.LO cs.SY eess.SY
Verification of Reachability Problems for Time Basic Petri Nets
基于时间的Petri网是一种用于实时系统建模的强大的形式主义，其中时间约束通过与转换相关联的标记的时间描述的时间函数来表示，表示可能的触发时间。我们介绍了一种技术，可达性分析的基础上建设的有限收缩的无限状态空间与这样一个模型。该技术构造了一个有限的符号可达图依赖于一种时间覆盖，并克服了现有的分析工具的限制，时间基本网络，反过来基于一个时间有界的检查（可能是无限的）可达树。该技术的一个关键特征是引入了时间匿名概念，该概念允许识别不影响模型演变的组件。一个运行的例子是在整个文件中使用草图的符号图的建设。图的构造算法已被自动化的Java工具集，在该文件中描述连同其主要功能和分析能力。描述一个真实世界的例子的用例已经被用来对技术和工具集进行基准测试。文中还介绍了试验的主要结果。
2014-09-09 cs.LO cs.SE
DNN Verification, Reachability, and the Exponential Function Problem
本文研究DNN验证的理论可计算性与复杂性，证明分段光滑激活函数下DNN验证可判定性等价于Tarski开放问题，并将线性算术规约下的验证问题归约为NP完全的DNN可达性问题。
2023-07-10 cs.CC cs.LO
Uncertainty Removal in Verification of Nonlinear Systems against Signal Temporal Logic via Incremental Reachability Analysis
U2IS, ENSTA, Institut Polytechnique de Paris（巴黎理工学院 U2IS）
本文通过增量可达性分析方法，解决非线性系统在验证信号时间逻辑规范时的不确定性问题，有效减少满足模糊性。
2026-09-28 cs.FL cs.LO
Mining Malware Specifications through Static Reachability Analysis
LIAFA, CNRS（法国国家科学研究中心LIAFA实验室）；Univ. Paris Diderot（巴黎狄德罗大学）
恶意软件（malware）的数量正在失控地增长。基于句法签名的检测无法应对这种增长，并且恶意软件签名数据库的手动构建需要被基于计算机学习的方法所取代。目前，捕获恶意行为语义的单个现代签名可以用来替换任意大量的老式语法签名。然而，教计算机学习此类行为是一项挑战。现有的恶意行为提取方法主要依赖于动态分析，但这种方法不能保证对所有恶意行为的覆盖。为了避开这个限制，我们展示了如何使用静态可达性分析来学习恶意软件签名。其思想是使用下推系统（可用于对二进制代码执行期间发生的堆栈操作进行建模）对二进制程序进行建模，使用可达性分析以树的形式提取行为，并使用从恶意软件文件的训练集中提取的树中常见的子树作为签名。为了检测恶意软件，我们建议使用树自动机来压缩存储恶意行为树，并检查从分析文件中提取的任何子树是否是恶意的。实验数据表明，我们的方法可以用来学习从恶意软件文件的训练集的签名，并使用它们来检测一个测试集的恶意软件是5倍的训练集的大小。
2013-12-17 cs.AI cs.CR cs.LO
Verification of Parametric Markov Automata under Time-bounded Reachability
Eindhoven University of Technology（埃因霍温理工大学）
针对参数化马尔可夫自动机（pMA），提出通过离散化为参数化马尔可夫决策过程（pMDP）并分析，解决时间有界可达性概率的合成问题，实现参数空间的满足/违反区域划分。
2026-06-23 cs.LO
Model-Checking of Linear-Time Properties Based on Possibility Measure
利用可能性测度研究了可能性Kripke结构下的LTL模型检验。首先介绍了可能性Kripke结构的概念和相关的可能性测度，然后研究了有限可能性Kripke结构线性时间可达性和重复可达性的模型检验.引入了可能性Kripke结构的标准安全性和非正则性，深入研究了正则安全性和非正则性的有限自动机验证问题。证明了有限可能性Kripke结构中正则安全性和非正则性的验证可以转化为本文所介绍的乘积可能性Kripke结构中可达性和重复可达性的验证。文中给出了几个算例来说明本文所提出的方法。
2016-09-25 cs.LO
Sampling-Based Verification of CTMCs with Uncertain Rates
我们采用不确定的参数CTMCs参数的过渡率和先验的参数值。先验对关于实际转换速率的不确定性进行编码，而参数允许转换速率之间的依赖性。从先验分布中采样参数值，然后产生一个标准的CTMC，我们可以计算相关的可达性概率。我们提供了一个原则性的解决方案，基于一种技术，称为双优化，以下问题：从一组有限的参数样本和用户指定的置信水平，计算预测区域的可达性概率。预测区域应该（以高概率）包含由任何附加样本诱导的CTMC的可达性概率。为了提高方法的可扩展性，我们采用标准的抽象技术，并调整我们的方法来支持近似的可达性概率。各种知名的基准测试的实验表明，该方法的适用性。
2022-06-21 cs.LO math.OC
Solving reachability problems on data-aware workflows
Fondazione Bruno Kessler（布鲁诺·凯斯勒基金会）；Free University of Bozen-Bolzano（博尔扎诺-博岑自由大学）
本文面向命令式数据感知业务流程的可达性验证，提出基于 Workflow Nets 扩展模型的框架，并将其语义映射到 Action Languages、Classical Planning 与 Model Checking，评估三类工具性能。
2020-09-03 cs.AI 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
Incremental Property Directed Reachability
本文提出增量式属性定向可达性算法IPDR，复用增量SAT求解器的先前验证结果，支持增量约束与松弛，在电路铺石和并行程序问题上性能优于Z3的SPACER，可大量复用实例间子句。
2023-08-23 cs.LO cs.SC
Checking Presence Reachability Properties on Parameterized Shared-Memory Systems
本文研究由任意数量异步进程组成的参数化共享内存系统的验证问题，证明基于轮次模型的存在性可达性质参数化验证是 PSPACE 完全的，而无轮次模型降至 NP 完全，并给出多项式时间可解的限制条件。
2023-07-31 cs.DC cs.FL cs.LO
Finite Model Finding for Parameterized Verification
在本文中，我们调查在何种程度上一个非常简单和自然的“可达性演绎”的方法，起源于安全的形式化方法的研究，是适用于大类的无限状态和参数化系统的自动验证。该方法是基于建模（参数化）状态之间的可达性演绎之间的适当的编码状态的一阶谓词逻辑的公式。安全性的验证被简化为一个寻找一阶公式的反模型的纯逻辑问题。后一项任务则委托给通用的自动化有限模型构建程序。本文首先对一类参数化线性阵列的有限自动机建立了有限反模型发现方法（FCM）的相对完备性。该方法被证明是至少一样强大的已知方法的基础上单调抽象和符号向后可达性。此外，我们扩展了该方法的相对完备性，并表明它可以解决所有的安全验证问题，可以解决传统的定期模型检验。
2010-11-26 cs.LO
Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
我们研究了验证有限连续时间马尔可夫链（CTMC）C对线性实时规范作为一个确定性的时间自动机（DTA）A有限或穆勒接受条件。我们要解决的中心问题是：C的路径集合被A接受的概率是多少，即，C满足A的可能性结果表明，在有限的验收标准，这等于在有限的分段确定性马尔可夫过程（PDP）的可达概率，而Muller验收标准，它符合终端强连通组件在这样的PDP的可达概率。定性验证显示相当于PDP的图形分析。在我们的PDP的可达性概率，然后其特征在于作为第二类Volterra积分方程系统的最小解，并示出近似的偏微分方程系统的解决方案。对于单时钟DTA，该积分方程系统可以被变换成线性方程系统，其中系数是常微分方程的解。由于系数实际上是CTMC中的瞬态概率，因此该结果意味着CTMC分析的标准算法足以验证单时钟DTA规范。
2011-03-27 cs.LO
Introducing H, an institution-based formal specification and verification language
这是一个简短的调查的发展，形式规格说明和验证语言H的科学部分的重点。H是一种现代的高度表达性的语言，它牢固地建立在先进的数学理论基础上，例如机构理论中Kripke语义学的内化。
2019-08-26 cs.LO math.LO
Certifying Almost-Sure Reachability in Unknown MDPs
Indian Institute of Technology Bombay（印度理工学院孟买分校）；Georgia Institute of Technology（佐治亚理工学院）
本文针对未知MDP，研究仅通过采样访问验证已有策略的几乎必然可达性，在非零转移概率下界p_min限制下可学习带PAC保证的证书，实验显示该条件偏保守。
2026-10-14 cs.AI cs.LO
Revisiting Reachability in Timed Automata
我们重新审视了实时验证的一个基本结果，即给定的时间自动机的配置之间的二进制可达性关系是可定义的整数和实数的线性算术。在本文中，我们给出了一个新的和更简单的证明这一结果，建立在著名的可达性分析的时间自动机涉及差分界矩阵。利用这个新的证明，我们给出了一个指数空间过程的模型检验的可达性片段的逻辑参数TCTL。最后我们证明了后一个问题是NEXPTIME困难的。
2017-04-18 cs.LO
Proceedings 9th International Workshop on Automated Specification and Verification of Web Systems
本卷包含第9届Web系统自动化规范和验证国际研讨会（WWV'13）的接受论文，该研讨会于6月6日在意大利佛罗伦萨举行，作为第8届分布式计算技术国际联合会议（DisCoTec 2013）的卫星活动。
2013-07-31 cs.LO cs.SE
Improved Undecidability Results for Reachability Games on Recursive Timed Automata
我们研究递归时间自动机（RTA）上的可达性游戏，推广Alur-Dill时间自动机的递归过程调用机制类似于递归状态机。对于具有两个或多个时钟的自动机，RTA上的可达性博弈中的胜者判定问题是不可判定的，而对于只有一个时钟的自动机，该问题是可判定的。Ouaknine和Worrell最近提出了一个实时验证的时间有界理论，声称对有界时间的限制恢复了与实时验证相关的几个关键决策问题的可判定性。我们重新审视了具有时间限制的递归时间自动机上的博弈，希望能恢复可判定性。然而，我们发现，这个问题仍然是不可判定的递归时间自动机与三个或更多的时钟。使用类似的证明技术，我们的特点是一个可判定性边境的推广RTA递归秒表自动机。
2014-08-26 cs.FL cs.LO
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications
我们介绍MCMAS-SLK，一个基于BDD的模型检查器的验证系统对规格表示在一个新的，认知的战略逻辑的变体。我们给出了规约语言的语法和语义，并介绍了一个标记算法的认知和策略逻辑模态。我们提供的检查器，也可以用于合成代理的策略，使系统满足规格的细节。我们评估的执行效率，通过讨论用餐密码协议和蛋糕切割问题的一个变种所获得的结果。
2014-05-16 cs.LO
Fundamental Limits in Formal Verification of Message-Passing Neural Networks
University of Kassel（卡塞尔大学）
输出可达性和对抗鲁棒性是神经网络最相关的安全属性之一。我们表明，在消息传递神经网络（MPNN）的背景下，一个常见的图神经网络（GNN）模型，形式化验证是不可能的。特别是，我们表明，输出可达的图分类MPNN，工作在图的无界大小，非平凡程度和充分表达节点标签，不能正式验证：有没有算法，正确回答（是或否），给定一个MPNN，是否存在一些有效的输入MPNN，使相应的输出满足给定的规格。然而，我们也表明，输出的可达性和对抗性的鲁棒性节点分类MPNN可以正式验证时，输入图的程度的限制是先验的。我们讨论了这些结果的影响，为了获得一个完整的图片的原则可能性，正式验证GNN，根据所涉及的GNN模型和输入输出规格的表现力。
2022-10-04 cs.LG cs.LO
What is Formal Verification without Specifications? A Survey on mining LTL Specifications
TU Dortmund University（多特蒙德工业大学）；University of Oxford（牛津大学）
本综述针对形式化验证中手动制定规约困难且易错的瓶颈，系统梳理并比较了从系统行为示例中自动挖掘线性时序逻辑（LTL）规约的最新技术与方法。
2025-01-27 cs.AI cs.FL cs.LO
A Practical Specification Language for Automatic Quantum Program Verification (Technical Report)
Institute of Information Science, Academia Sinica（中央研究院資訊科学研究所）；Graduate Institute of Electronics Engineering, National Taiwan University（国立台湾大学电子工程学研究所）；Faculty of Information Technology, Brno University of Technology（布尔诺理工大学信息技术学院）
本文提出了一种扩展的集合基规范语言和转换算法，通过控制自动机构造和量子位重排，实现线性复杂度的量子程序自动验证。
2026-05-07 cs.FL cs.LO
On The Reachability Problem for Recursive Hybrid Automata with One and Two Players
受有限状态机有界模型检验框架成功的启发，Ouaknine和Worrell提出了实时验证的时间有界理论，认为对有限时间的限制恢复了与实时验证相关的几个关键决策问题的可判定性。为了支持这一理论，最近的列表不可判定的问题证明在时间有界的限制下可判定的是相当令人印象深刻的：语言包含的时间自动机，空问题交替时间自动机，空问题矩形混合自动机。我们研究的目的是恢复一般递归时间自动机的可判定性-也许递归混合自动机-在时间有界的限制下，以提供一个有吸引力的验证框架，强大的建模环境，如Stateflow/Simulink。不幸的是，然而，我们回答这个问题的否定表明，时间有界的可达性问题保持不可判定的递归时间自动机与五个或更多的时钟。虽然坏消息继续，即使当一个考虑行为良好的子类的递归混合自动机，我们恢复可判定性考虑递归混合自动机与有界上下文使用通过引用机制，或通过限制变量的数量为2，率在$\{0,1\}$。
2014-08-15 cs.FL cs.LO
Q-Learning for Reachability in MEC-Free MDPs
Georgia Institute of Technology（佐治亚理工学院）
本文提出Quasar，首个无模型Q学习算法，用于无最大端分量MDP的可达性，通过时序差分更新实现渐近最优，内存从O(|S|^2|A|)降至O(|S||A|)，样本效率显著优于基于模型方法。
2026-10-02 cs.AI cs.LG cs.LO
Reachability problems for communicating finite state machines
本文讨论了一种常用的通信协议状态转移模型的可达性验证问题，该模型由有限状态机和潜在无界的FIFO通道组成。虽然简单可达性问题对于一般的无界信道协议是不可判定的，但对于具有可识别信道性质的协议是可判定的。对于具有合理信道特性的协议，可判定性问题是开放的。
2012-03-20 cs.LO cs.NI
Towards platform-independent specification and verification of the standard trigonometry functions
研究计划“标准数学函数形式化规范与验证的平台无关方法”旨在开发一种增量式组合方法来规范和验证标准数学函数，如sqrt，cos，sin等。平台无关意味着我们试图设计一种相对简单的计算机算法公理化，和整数算术（即实数和有理数的域R和Q，整数环Z），但既不指定计算机算术的基，也不指定数字表示的格式。递增性意味着我们从最简单的最简单的规范开始，最简单的易于验证的实数算法，并以计算机算法的现实规范和验证结束。我们称我们的方法为组合，因为我们从手册开始（纸笔）验证某些选定的实数算法，然后将这些算法和验证作为计算机算法及其人工验证的草稿和证明大纲，最后，利用计算机辅助校对系统对手工校对进行了验证（以避免诉诸“显而易见”，这在人类携带的证据中非常常见）。在本文中，我们提出了第一个步骤，对一个平台无关的增量相结合的方法，规范和验证的标准函数的cos和sin，实现数学三角函数的cos和sin。
2019-01-10 cs.LO
Automatic Verification of Parametric Specifications with Complex Topologies
本文的重点是降低验证的复杂性，利用模块化在各个层次上：在规范，验证，和结构。对于规范，我们使用的模块化语言CSP-OZ-DC，它允许我们解耦验证任务有关的数据从那些有关的持续时间。在验证级别，我们利用模块化的定理证明丰富的数据结构，并使用此不变检查。在结构层面上，我们分析了模块化验证的系统组成的各种组件的相互作用的可能性，我们说明了这些想法，通过自动验证安全性能的案例研究，从欧洲训练控制系统标准，它扩展了以前的例子，包括一个复杂的轨道拓扑结构与列表的轨道段和列车与不同的路线。
2010-10-08 cs.LO cs.SE
Verification of Flat FIFO Systems
本文通过归约证明平坦FIFO机器及有损变体的可达性等问题为NP完全，并构造互模拟系统以支持模型检测，为FIFO机器验证工具奠定基础。
2020-10-12 cs.CC cs.LO
On parametrized verification of asynchronous, shared-memory pushdown systems
我们考虑参数化的异步共享内存下推系统的模型，在[海牙'11]中介绍。在最近的一系列论文中，已经证明了该模型的可达性是PSPACE完全的[Esparza，Ganty，Majumdar'13]，并且活性在NEXPTIME中是可判定的[Durand-Gasselin，Esparza，Ganty，Majumdar'15]。我们在这里证明了活性问题是PSPACE完全的。我们还介绍了普遍的可达性问题。我们证明了它是可判定的，并且是coNEXPTIME完全的。最后，利用这些结果，我们证明了在NEXPTIME中，满足一定条件的执行轨迹的验证正则性也是可判定的。
2016-07-15 cs.FL cs.LO
Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS
使用算法由于萨夫拉分布式终止检测作为一个运行的例子，我们提出了验证TLA+编写的规范的主要工具。检查他们的互补优势和弱点，我们建议一个工作流程，支持不同类型的分析，并可以适应所需程度的信心。
2022-11-14 cs.LO
Algorithmic Verification of Continuous and Hybrid Systems
CNRS-VERIMAG University of Grenoble（格勒诺布尔大学 CNRS-VERIMAG）
本文介绍可达性计算，一种用于连续和混合系统验证的计算技术，能替代无限次模拟。
2014-02-27 cs.FL cs.LO cs.NA
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
$\{log\}$: Applications to Software Specification, Prototyping and Verification
本文档将介绍如何将Z规范转换为$\{log\}$，以及如何使用$\{log\}$运行模拟和自动化证明。这可以帮助其他规约语言（如B和VDM）的用户按照相同的方式使用$\{log\}$。介绍相当非正式，面向用户。更多的技术和正式的介绍可以在作者发表的论文中找到。我们还假设读者至少对Z符号有基本的了解。
2021-03-27 cs.LO cs.SE
Lessons Learned From Microkernel Verification -- Specification is the New Bottleneck
软件验证工具近年来变得更加强大。甚至大型复杂系统的验证也是可行的，如L4.verified和Verisoft XT项目所示。尽管如此，大型软件系统的功能验证是罕见的-原因超出了大规模的验证工作所需的大小。在本文中，我们报告的经验教训，验证大型软件系统的基础上获得的经验，在Verisoft XT项目的微核验证。我们讨论了一些问题，阻碍广泛引入形式化验证在软件生命周期过程。
2012-11-27 cs.LO cs.SE
Proceedings 11th International Workshop on Automated Specification and Verification of Web Systems
这些会议记录包含在2015年6月23日在挪威奥斯陆举行的第11届Web系统自动化规范和验证国际研讨会（WWV 2015）上提交的论文，作为第20届形式化方法国际研讨会（FM 2015）的卫星研讨会。WWV是一个年度跨学科论坛，研究人员来自以下领域：声明式，基于规则的编程，形式化方法，软件工程和基于Web的系统。该研讨会促进这些领域的混合方法的交叉和进步。
2015-08-14 cs.LO cs.PL cs.SE
Towards the Formal Specification and Verification of Maple Programs
在本文中，我们提出了我们正在进行的工作和初步结果的形式规范和验证的MiniMaple（一个重要的子集Maple轻微扩展）程序。我们工作的主要目标是在这些程序中找到行为错误。通过静态分析确定其规格。这项任务是更复杂的广泛使用的计算机代数语言，如Maple，因为这些是从根本上不同于经典的语言：它们支持非标准类型的对象，如符号，未评估的表达式和多项式，并需要抽象的计算机代数概念和对象，如环和排序等作为一个出发点，我们已经定义和形式化的语法，语义，类型系统和规约语言的MiniMaple。
2012-07-10 cs.LO cs.MS cs.PL
Complexity of Verification and Synthesis of Threshold Automata
Technical University of Munich（慕尼黑工业大学）
本文研究了阈值自动机的验证与合成问题的复杂性，证明了多个核心问题的计算复杂度，并提出了一种基于Presburger公式的新算法。
2025-11-28 cs.DC cs.LO
Specification of State and Time Constraints for Runtime Verification of Functions
用于运行时验证的技术通常利用规约语言，其（i）合理地表达，以及（ii）相对抽象（即，它们在将它们与被监视的系统分离的抽象级别上操作）。受CERN高能物理实验数据处理中监控系统问题的启发，提出了一种规约语言--控制流时序逻辑（CFTL），它的显著特点是与程序控制流紧密耦合，用于编写规范。这种耦合导致了大多数时态逻辑所使用的典型的高抽象级别的偏离。其余的贡献是一个静态分析为基础的仪器过程，这是特定于CFTL和它的公式的结构，和监测算法。报告最后分析了CFTL及其监控算法应用于一些示例程序时。
2018-06-08 cs.LO
Abstract Framework for All-Path Reachability Analysis toward Safety and Liveness Verification (Full Version)
Graduate School of Informatics, Nagoya University（名古屋大学大学院信息学研究科）
本文重构了针对ARs的部分有效性抽象框架，建立了ARs和LCTRSs部分有效性的推理规则一一对应关系，并引入总有效性概念以支持活性验证，证明了证明图的无环性是总有效性的充要条件。
2026-06-29 cs.LO
Modeling and Verification of Infinite Systems with Resources
我们考虑资源消耗递归程序的形式化验证。我们引入前缀替换系统与非负整数计数器，可以增加和重置为零，作为一个正式的模型，这样的程序。在这些系统中，我们调查的可达性问题的资源消耗的界限。基于这个问题，我们引入了具有资源的关系结构和这些结构上的定量一阶逻辑。我们定义了资源自动结构作为这些结构的子类，并提供了一种有效的方法来计算这个子类上的逻辑的语义。随后，我们使用这个框架来解决资源前缀替换系统的有界可达性问题。我们实现了这一结果，通过扩展著名的饱和度的方法来注释前缀替换系统。最后，我们提供了一个连接到逻辑成本的研究-WMSO。
2013-12-14 cs.LO
pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis
University of California, Berkeley（加州大学伯克利分校）
提出pacSTL框架，结合PAC有界可达集预测与区间STL，通过优化问题计算原子鲁棒性上下界并传播，实现规范级别的PAC有界鲁棒性评估，用于不确定动态系统的验证与监控。
2026-07-24 cs.LO cs.RO
Complete Robust Hybrid Systems Reachability
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）
本文提出鲁棒微分动态逻辑，证明其对混合系统可达性问题的绝对完备性，为精确语义的混合系统提供自动验证方法。
2026-07-24 cs.LO
Specification and Verification of Distributed Embedded Systems: A Traffic Intersection Product Family
分布式嵌入式系统（DES）不再是例外;它们是许多应用领域的规则，如航空电子，汽车工业，交通系统，传感器网络和医疗设备。由于状态空间爆炸和实时特性的需要，形式化的DES规范和验证具有挑战性。本文报告了一个广泛的基于行业的案例研究，涉及DES产品系列的行人和汽车4路交通路口，其中自主设备通过异步消息传递进行通信，而无需集中控制器。已使用实时Maude及其模型检验功能正式验证了需求文档中非正式规定的所有安全需求和活性需求。
2010-09-22 cs.LO
Proceedings 10th International Workshop on Automated Specification and Verification of Web Systems
这些会议记录包含在第10届Web系统自动规范和验证国际研讨会上提交的论文（WWV 2014），于2014年7月18日在奥地利维也纳举行，作为联邦逻辑会议的卫星研讨会（FLoC 2014），与第七届自动推理国际联合会议（IJCAR 2014）相关，作为维也纳逻辑之夏（VSL 2014）的一部分。WWV是一个年度研讨会，旨在提供一个跨学科的论坛，以促进交叉施肥和混合方法的发展，这些方法利用基于规则的编程，正式方法，软件工程和面向Web的研究的概念和工具。
2014-09-08 cs.LO cs.PL cs.SE
OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse
OpenJML是一个检查Java程序的代码和规范的工具。我们描述了我们的经验，建立在JML，OpenJDK和Eclipse的基础上的工具，以及在基于规范的软件验证的许多进步。该实现展示了直接在软件开发IDE中集成规范工具的价值，以及尽可能多地自动化任务的价值。该工具，虽然仍在进行中，现在已被用于几个大学水平的课程，软件规范和验证，并对现有的Java程序的小规模研究。
2014-04-26 cs.LO cs.PL cs.SE
