The Complexity of Satisfiability Checking for Symbolic Finite Automata
本文研究符号有限自动机的可满足性问题，通过将其分解为输入字符理论与接受单词索引的单子二阶理论，获得了该自动机类及其线性算术约束扩展的紧计算复杂度界限。
2023-06-30 cs.LO
Symbolic model checking of tense logics on rational Kripke models
本文引入了有理Kripke模型类，研究了基本时态逻辑Kt的符号模型检验及其在该类模型中的一些扩展。有理Kripke模型基于（通常是无限的）有理图，顶点由某些正则语言中的单词标记，转换由异步双头有限自动机（也称为有理转换器）识别。在理性Kripke模型中，每个原子命题都在一组规则的状态中求值。证明了Kt的每个公式在每个有理Kripke模型中都有一个有效的可计算正则扩张，从而证明了有理Kripke模型中Kt的局部模型检验和全局模型检验是可判定的.这些结果被提升到Kt的一些扩展。我们研究并部分确定了模型检验过程的复杂性。
2008-10-30 cs.LO
Significant Diagnostic Counterexamples in Probabilistic Model Checking
提出了一种新的马尔可夫链和马尔可夫决策过程概率模型检验中的反例生成技术。反例中的（有限）路径在可能向用户提供类似调试信息的证人中被分组在一起。我们列出了五个属性，证人应该满足，以作为调试援助有用：相似性，准确性，独创性，重要性和有限性。我们的见证者包含在强连接组件之外表现相似的路径。本文展示了如何计算这些证人减少的问题，生成反例的一般属性在马尔可夫决策过程中，在几个步骤，生成反例的可达性属性在非循环马尔可夫链的简单问题。
2008-06-06 cs.LO cs.PF
Counterexample Generation for Infinite-State Chemical Reaction Networks
反例生成是模型检验过程中不可缺少的一部分。在随机模型检验中，反例生成是一个具有挑战性的问题，因为它是不够的，找到一个单一的轨迹，违反了给定的性质。相反，一个潜在的大集合的痕迹有足够的概率违反的性质需要found.This本文考虑反例生成化学反应网络（CRN）模型与潜在的无限状态空间。提出了一种基于SMT求解的有界模型检验的CRN反例生成方法。它旨在找到给定模型的一小组违反属性的路径，使得它们共同具有高于给定阈值的总概率。一个独特的挑战是由于CRN的高度连接的状态空间，其中一个反例只是所有违反属性的路径的一个很小的子集。为了解决这些挑战，本文提出了一些优化，包括分而治之的技术，以扩大大型CRN模型的反例生成方法。本文报道了一些无限状态CRN模型的实验结果。
2022-07-11 cs.LO
Generating Counterexamples for Model Checking by Transformation
反例解释了为什么所需的时间逻辑属性无法保持。反例的产生被认为是模型检验作为一种验证技术的主要优点之一。此外，当模型检验确实成功地验证了属性时，通常不存在可用作已验证属性的证据的独立可检验见证。在此之前，我们已经展示了程序转换技术如何用于验证反应系统的安全性和活性特性。然而，没有反例或证人使用所描述的技术产生。在本文中，我们将讨论这个问题。特别是，我们展示了如何程序转换技术蒸馏可以用来促进反应系统的时间属性的反例和证人的建设。示例系统的目的是相互排斥模型进行分析，使用这些技术的安全性（相互排斥）和活性（非饥饿），与反例生成的那些属性不举行。
2016-07-08 cs.LO cs.SE
SMT-based Symbolic Model-Checking for Operator Precedence Languages
针对现有POTL显式状态模型检测方法可扩展性差的问题，本文提出首个基于SMT的符号化方法，将POTL公式与程序模型编码为SMT公式，通过求解器以有界模型检测方式搜索反例轨迹，实验验证了方案有效性。
2024-05-18 cs.LO
Making Abstraction Refinement Efficient in Model Checking
摘要抽象是模型检验中处理状态空间爆炸问题的重要策略之一。在抽象模型中，虽然状态空间大大缩小，但是在这样的模型中找到的反例可能不是真正的反例。对于经常涉及NP-难状态分离问题的抽象模型，需要进一步细化。本文提出了一种新的方法，通过增加额外的变量的抽象模型的细化。该方法不仅避免了NP-hard状态分离问题，而且得到了一个更小的精化抽象模型。
2010-07-21 cs.LO
Tracy, Traces, and Transducers: Computable Counterexamples and Explanations for HyperLTL Model-Checking
针对HyperLTL模型检测仅提供二元结果的问题，提出基于Skolem函数的两种反例与解释范式，分别实现完备性（限最终周期轨迹）和通用性（图灵机可计算函数），并证明相关可判定性且能计算转换器。
2024-11-26 cs.FL cs.LO
Linear Encodings of Bounded LTL Model Checking
研究线性时序逻辑的有界模型检验问题。我们提出了几个有效的编码，具有大小线性的界限。此外，我们展示了如何编码可以扩展到LTL与过去的运营商（PLTL）。广义编码仍然是线性的大小，但不能检测最小长度的反例。通过使用虚拟展开技术可以捕获最小长度的反例，然而，在规范中编码的大小是二次的。我们还扩展虚拟展开的Buchi自动机，使他们能够接受最小长度的反例。我们的BMC编码可以是增量的，以便从增量SAT技术中受益。通过相当小的修改，增量编码可以通过终止检查进一步增强，允许我们使用BMC证明属性。实验清楚地表明，我们的新编码大大提高了BMC的性能，特别是在增量编码的情况下，并且它们在发现错误方面非常有竞争力。对活性到安全性转换的分析揭示了本文中BMC编码的许多相似之处。使用基于BDD的不变式检查的活性到安全性的转换结果在一个有效的方法来找到最短的反例，补充基于BMC的方法。
2006-11-16 cs.LO
SMT Queries Decomposition and Caching in Semi-Symbolic Model Checking
在半符号（控制-显式数据-符号）模型检验中，状态空间爆炸问题通过位向量理论上的一阶公式表示状态集来解决。在这种模型检验方法中，大部分验证时间都花在SMT求解器上，用于确定量化查询的可满足性，这些量化查询表示符号状态的相等性。在本文中，我们介绍了一个新的计划分解的符号状态，它可以用来显着提高任何半符号模型检查器的性能。使用分解，与原始情况相比，模型检查器可以向求解器发出更简单和更小的查询。一些SMT调用甚至可以完全避免，因为一些简化公式的满足可以从语法上决定。此外，分解允许用于量化公式的高效缓存方案。为了支持我们的理论贡献，我们展示了我们的模型检查器SymDIVINE的性能增益的一组例子，从软件验证比赛。
2017-11-20 cs.LO cs.PL
Integrating Loop Acceleration into Bounded Model Checking
本文将循环加速技术动态集成到基于SMT的有界模型检测中，通过添加捷径和阻塞子句，既能快速发现深层反例，又能在BMC发散时证明安全性，实验表明其在证明不安全性方面具有竞争力。
2024-08-09 cs.LO
Symbolic Simulation-Checking of Dense-Time Systems
直观地说，一个（实现）自动机被一个（规范）自动机模拟，如果实现自动机的每个外部可观察的转换也可以由规范自动机完成。在这项工作中，我们提出了一个符号算法的时间自动机的模拟检查。我们首先提出了一个模拟检查程序，操作状态空间，表示与凸多面体，时间自动机。然后，我们提出的技术来表示这些中间结果凸多面体的区域，并使该过程的算法。然后，我们讨论如何在实现自动机中处理芝诺状态。最后，我们完成了算法的实现，并在实验中报告了我们的算法的性能。
2006-10-13 cs.LO cs.SE
The Complexity of Checking Non-Emptiness in Symbolic Tree Automata
该研究将符号树自动机的可满足性问题分解为两类理论的可满足性问题，进而得到该类自动机及其带线性算术约束扩展的判定问题的紧计算复杂度界。
2023-11-09 cs.FL cs.LO
Explaining Counterexamples with Giant-Step Assertion Checking
在程序的演绎验证过程中，识别证明失败的原因是困难的：它可能是由于程序中的不正确，程序注释中的不完整性，或者证明器的不完整性。解决证明失败所需的更改取决于其类别，但证明器无法提供任何分类帮助。当使用SMT求解器来履行证明义务时，该求解器可以从失败的尝试中提出一个模型，从中可以导出一个可能的反例。但反例可能是无效的，在这种情况下，它可能会增加更多的混乱而不是帮助。为了检查反例的有效性和分类证明失败，我们提出了两种不同的语义下的运行时断言检查（RAC）执行之间的比较，使用反例作为一个预言。第一次RAC执行遵循正常的程序语义，违反程序注释表示程序中存在错误。第二个RAC执行遵循一个新的“giant-step”语义，它既不执行循环，也不执行函数调用，而是从oracle中检索返回值和修改变量的值。只有在巨步执行下才能观察到的程序注释的违反表征了程序注释的不完整性。我们实现了这种方法在Why 3平台的演绎程序验证和评估它使用的例子从以前的文献。
2021-08-06 cs.LO cs.PL
From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
我们提出了一个有界等价性验证技术的高阶程序与局部状态。该技术结合了完全抽象的符号环境互模拟类似的符号游戏语义，新的技术，轻量级的状态不变的注释。这产生了没有假阳性或假阴性的等效性验证技术。该技术是有界完备的，因为所有的不等式都是自动检测到足够大的界限。此外，几个硬等价证明自动或后被注释与状态不变量。我们在一个名为Hobbit的工具原型中实现了该技术，并使用一组广泛的新的和现有的示例对其进行基准测试。霍比特人可以证明许多经典的等价关系，包括所有迈耶和西伯的例子。
2021-10-22 cs.LO cs.PL
A Backward-traversal-based Approach for Symbolic Model Checking of Uniform Strategies for Constrained Reachability
自从交替时间时序逻辑（ATL）被引入以来，许多逻辑被提出来推理系统中智能体的不同策略能力。特别是，一些逻辑已经被设计成这样的代理商的统一的无记忆策略的原因。这些策略是智能体可以通过只看他们从当前状态观察到的东西来有效地发挥作用的策略。ATL_ir可以被看作是推理这种统一策略的核心逻辑。然而，它的模型检查问题是困难的（它需要对NP预言机的多项式次数的调用），并且解决它的实用算法直到最近才出现。本文提出了一种模型检验统一无记忆策略技术。现有技术通过系统的前向遍历从感兴趣的状态（诸如初始状态）构建策略。另一方面，所提出的方法通过向后遍历从目标状态构建获胜策略，确保只探索统一的策略。然而，从头开始构建策略将其适用性仅限于受限的可达性目标。本文详细介绍了这种方法，并将其与现有的方法实现到一个基于BDD的框架实验比较。这些实验表明，该技术是有竞争力的情况下，它可以处理。
2017-09-07 cs.LO
Formal Verification of Safety Properties Using Interpolation and k-induction
本技术报告介绍了使用SAT/SMT求解器的两种符号模型检验算法的实现，即基于插值的模型检验和基于k-归纳的模型检验。并对这两种模型检验算法进行了比较分析。
2022-07-04 cs.LO
Symbolic bisimulation for quantum processes
利用文献中提出的互模拟概念，为了检验两个量子过程是否互相似，我们必须用任意量子态实例化它们的自由量子变量，并验证结果组态的互相似性。这使得从算法的角度来看，检查双相似性是不可行的，因为量子态构成了一个连续统。在本文中，我们直接在量子操作层次上引入了一种量子过程的符号操作语义，它允许我们描述量子过程之间的互模拟，而无需求助于量子态。我们表明，这里定义的符号互模拟是等价的开放互模拟量子过程在以前的工作中，当考虑强互模拟。提出了一种符号基双相似性检验算法。基于Hennessy-Milner逻辑对量子过程的扩展，我们给出了量子双相似性的模态逻辑刻画。
2012-02-21 cs.LO
Symbolic Model Checking in External Memory
本研究为外部存储器BDD包Adiar扩展单调变量替换支持以实现关系积运算，优化后小BDD模型检测速度最高提47%，其I/O高效性使其受内存影响小，大实例下远快于同类工具CAL。
2025-05-16 cs.DS cs.LO
Bug Hunting By Computing Range Reduction
我们描述了一种模型检验的方法，称为计算范围缩减（CRR）。CRR方法基于子句的推导，该子句以至少保留一个反例（如果有的话）的方式减少可达状态的迹集。这些子句是通过称为部分量词消去（PQE）的技术导出的。给定一个数n，CRR方法找到一个长度小于或等于n的反例，或者证明这样的反例不存在。我们的实验表明，我们开发的PQE求解器可以有效地应用于现实的基准转换关系的约束条款的推导。CRR方法最吸引人的特征之一是它可以找到长反例。在这个领域，它可以击败模型检查器计算可达状态（或它们的近似值，如IC3）或基于SAT的有界模型检验方法。PQE不能有效地模拟SAT求解器。这一点很重要，因为当前模型检验的研究主要是基于SAT的算法。CRR方法提醒人们不要把所有鸡蛋放在一个篮子里。
2014-10-11 cs.LO
Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model Checking Dynamic Epistemic Logic
University of Groningen（格罗宁根大学）；University of Amsterdam（阿姆斯特丹大学）
本文提出用ZDDs替代BDDs对动态认知逻辑中的Kripke模型进行符号编码，并在三个经典多智能体谜题上验证了该方法可显著降低模型检测的内存使用。
2023-07-11 cs.AI cs.LO
PrIC3: Property Directed Reachability for MDPs
IC 3是符号模型检验的一次飞跃。本文提出了PrIC 3（发音为pricy-three），一个保守的扩展IC 3的符号模型检验的MDP。我们的主要重点是发展PrIC 3的理论基础。此外，我们还介绍了PrIC 3的第一个实现，包括IC 3的关键成分，如泛化，重推和传播。
2020-05-18 cs.LO
Visual Analysis of Hyperproperties for Understanding Model Checking Results
模型检查器提供用于证明系统的数学模型满足给定规范的算法。如果发生冲突，则返回一个显示错误行为的反例。理解这些反例是具有挑战性的，特别是对于超属性规范，即，将系统的多个执行相互关联的规范。我们的目标是通过我们的HyperVis工具，它提供了给定的模型，规范和反例的交互式可视化，以促进这种反例的可视化分析。在迭代和跨学科的设计过程中，我们开发了可视化解决方案，可以有效地传达模型检验结果的核心方面。具体来说，我们引入二进制值的图形表示，以提高模式识别，颜色编码，以更好地指示相关方面，视觉增强的文本描述，以及广泛的跨视图突出显示机制。此外，通过对反例的潜在因果分析，我们还能够识别导致违规的值，并将这些知识用于改进编码和突出显示。最后，分析人员可以直接在HyperVis中修改超属性和系统的规范，并启动新版本的模型检验。结合起来，这些特性显著地支持分析人员理解导致反例的错误以及迭代所提供的系统和规范。我们使用HyperVis进行了多个案例研究，并在定性反馈会议中与领域专家进行了测试。参与者的积极反馈证实了与基于文本的手册现状相比的显著改进以及该工具在解释超性质方面的价值。
2021-08-08 cs.HC cs.LO
Combining Explicit and Symbolic Approaches for Better On-the-Fly LTL Model Checking
我们提出了两种新的混合技术，取代同步产品中使用的自动机理论方法的LTL模型检验。建议的产品是明确的图形的聚集（符号集的状态），可以解释为Büchi自动机。这些混合方法一方面允许使用经典的空检查算法并在运行中构建图，另一方面，由于聚集体的符号表示，具有状态空间的紧凑编码。符号观测产品假设全局断续属性（例如，LTL \ X）来聚合状态。自循环聚合产品}不要求属性是全局断续的（即，它可以处理完整的LTL），但在可能的情况下动态地检测和利用一种形式的口吃。我们的实验表明，这两个变种，而彼此无法比拟的，可以优于其他现有的方法。
2011-06-28 cs.FL cs.LO
Dynamic Reductions for Model Checking Concurrent Software
并行程序的符号模型检验是解决交织爆炸问题的有效方法。我们提出了一个动态减少技术，以避免不必要的交织。通过扩展Lipton的原始工作与双相似性的概念，我们容纳动态事务，从而减少依赖于静态分析，这是一个严重的瓶颈，在其他减少技术的准确性。结合符号模型检验和动态约简技术已被证明是具有挑战性的，在过去。尽管如此，我们的通用归约定理使我们能够推导出一种有效的符号编码，我们为IC3和BMC实现了这种编码。实验证明了几个案例研究和一个大的SVCOMP基准动态减少的权力。
2016-11-28 cs.FL cs.LO
Debugging of Markov Decision Processes (MDPs) Models
在模型检验中，反例被认为是一种有价值的调试工具。在概率模型检验（PMC）中，反例的生成具有定量的特点. PMC中的反例是一组路径，其中路径公式成立，并且它们的累积概率质量违反概率阈值。然而，理解反例并不是一件容易的事情。在本文中，我们解决的任务，反例分析马尔可夫决策过程（MDP）。我们提出了一个辅助诊断方法的基础上的因果关系，责任和责备的概念概率反例。给定一个不适用于MDP模型的概率CTL（PCTL）公式的反例，此方法将引导用户找到导致违规的模型的最相关部分。
2016-08-29 cs.LO cs.SE
SMT-based Model Checking for Recursive Programs
提出了一种基于SMT的递归程序安全性验证的符号模型检验算法。该算法是模块化的，并单独分析程序。与其他基于SMT的方法不同，它既保持了程序摘要的“过度近似”，也保持了程序摘要的“欠近似”。欠近似用于分析过程调用，而无需内联。过近似用于阻止不可行的反例和检测收敛到一个证明。我们表明，程序和属性的可判定理论，该算法是保证找到一个反例，如果存在的。然而，效率依赖于用于量词消去（QE）的预言。对于布尔程序，该算法是一个多项式决策过程，匹配最佳BDD算法的最坏情况的界限。对于线性算术（整数和有理数），我们通过“懒惰地”应用QE给出了算法的有效实例。我们使用现有的插值技术来过度近似QE，并引入“基于模型的投影”来欠近似QE。在SV-COMP基准测试上的实验结果表明，该算法在最新水平上有了显著的改进。
2014-05-25 cs.LO
Satisfiability Checking and Symbolic Computation
符号计算和可满足性检验被视为独立的研究领域，但它们在算术理论决策过程的开发、实现和应用方面有着共同的兴趣。尽管有这些共同点，但这两个社区目前只有微弱的联系。我们引入了一个新的项目SC-广场，以在该地区建立一个联合社区，并得到新接受的同名欧盟（H2020-FETOPEN-CSA）项目的支持。我们的目标是通过创建共同的平台，启动互动和交流，确定共同的挑战，并制定共同的路线图，加强这些社区之间的联系。这张摘要和随附的海报描述了该项目的动机和目标，并报告了第一批活动。
2016-07-23 cs.LO cs.SC
Satisfiability Checking meets Symbolic Computation (Project Paper)
符号计算和可满足性检验是两个研究领域，两者在算术理论决策过程的发展、实现和应用方面有着各自的科学重点，但也有着共同的兴趣。尽管有共同点，但这两个社区的联系相当薄弱。我们新接受的SC-square项目（H2020-FETOPEN-CSA）的目的是通过创建共同平台，启动互动和交流，确定共同挑战，以及开发从理论到工具和（工业）应用的共同路线图来加强这些社区之间的联系。在本文中，我们报告的目标和该项目的第一次活动，并正式确定了一些相关的挑战，为统一的SC广场社区。
2016-07-27 cs.LO cs.SC
Software Model Checking with Explicit Scheduler and Symbolic Threads
在许多实际的应用领域中，软件被组织成一组线程，其激活是排他性的，并由一个合作的调度策略控制：线程执行，没有任何中断，直到它们终止或明确地将控制权交给调度程序。这种软件的形式化验证提出了重大挑战。一方面，每个线程可能有无限的状态空间，并且可能需要抽象。另一方面，调度策略通常对于正确性很重要，并且基于抽象调度器的方法可能导致精度损失和误报。不幸的是，将问题转化为纯粹的顺序软件模型检验问题对于现有技术来说是非常低效的。我们提出了一种利用这些程序的内在结构的软件模型检验技术。每个线程都被转换成一个单独的顺序程序，并通过惰性抽象进行象征性的探索，而整体验证则由调度程序的直接执行来协调。该方法是通过过滤的探索调度器与偏序约简的集成优化。该技术，称为ESST（显式线程，符号线程）已实施和实验评估的一组重要的基准。结果表明，ESST技术是更有效的方式比软件模型检验应用于序列化程序，和偏序约简可以导致进一步的性能改善。
2012-07-31 cs.LO cs.PL
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
用非线性实算术（NRA）检验设计（表示为转移系统）的模型检验不变性质是一个重要而又困难的问题。一方面，NRA是一个难以解决的理论，另一方面，大多数强大的模型检验技术缺乏对NRA的支持。在本文中，我们提出了一个反例引导的抽象细化（CEGAR）的方法，利用微分的线性化技术，使使用成熟和有效的模型检验算法的过渡系统的线性实数运算（LRA）与未解释的功能（EUF）。实证评估的结果证实了这种方法的有效性和潜力。
2018-01-26 cs.LO
Comparing State-Representations for DEL Model Checking
本文比较了 DEL 模型检查中符号结构和心理程序的表示方法，证明了其理论复杂性，并提供了两种转换的直接方法。
2025-11-27 cs.LO cs.MA
Towards Symbolic Factual Change in DEL
我们扩展了符号模型检验的动态认知逻辑（DEL）的事实变化。我们的Transformers提供了一个紧凑的表示动作模型的前置和后置条件，为S5和一般情况下。该方法可以实现使用二进制决策图，我们希望它能提高模型检验性能。作为一个例子，我们给萨利-安妮错误信念任务的象征性表示。
2019-12-23 cs.LO cs.SC
Irene: Equivalence Checking of Hybrid Quantum Programs via Structure-Preserving Symbolic Reduction
Shanghai Jiao Tong University（上海交通大学）
提出Irene框架，通过保结构符号化简在门级、混合路径和及密度核三个层次验证混合量子程序等价性，在1982个程序对中解决79.92%，并发现15个编译器缺陷。
2026-09-30 cs.LO cs.PL cs.SE
Debugging Smart Contract's Business Logic Using Symbolic Model-Checking
智能合约是在区块链内部运行的一种特殊类型的程序。它们是不可变和透明的，提供了实现容错和抗审查服务的方法。不幸的是，它的不变性导致了一个严重的挑战，即在区块链中发布之前，确保业务逻辑和实现是正确的。几起重大事故确实表明，这项技术的用户需要特殊的工具来验证智能合约的正确性。现有的自动检查器只能检测已知的实现错误，而将业务逻辑正确性问题远远抛在一边。在这项工作中，我们提出了一个象征性的模型检验技术，以及一个正式的规格说明方法的一个子集的Solidity程序设计语言，能够表达状态属性和跟踪属性，后者构成了一个弱的类比的时间属性。我们在MiniDAO智能合约上评估了所提出的技术，MiniDAO是臭名昭著的TheDAO的年轻兄弟。我们的概念验证能够在几秒钟内检测到这个智能合约的业务逻辑中的一个重要错误。
2018-12-03 cs.CR cs.LO cs.PL
Symbolic and Structural Model-Checking
本文提出结合SMT过近似、无记忆采样欠近似和结构化简规则，使模型检验复杂度与网结构而非状态空间成正比，并在2020年模型检验竞赛中赢得可达性查询和死锁检测。
2021-12-18 cs.DC cs.FL cs.LO
Automatic Abstraction in SMT-Based Unbounded Software Model Checking
基于欠近似和SMT求解器的软件模型检查器在验证安全性（即可达性）属性方面非常成功。它们结合了两个关键思想-（a）“具体性”：在一个下近似的反例是一个反例，以及在原来的程序，和（b）“泛化”：一个下近似的安全性证明，由SMT求解器，是可推广到原程序的安全性证明。在本文中，我们提出了一个“自动抽象”与近似驱动的框架。我们探讨了两种迭代的方法来获得和细化抽象-“基于证明”和“基于反例”-并展示了它们如何组合成一个统一的算法。据我们所知，这是基于证明的抽象的第一个应用程序，主要用于验证硬件，软件验证。我们已经实现了一个原型的框架使用Z3，并评估它的许多基准软件验证比赛。我们的实验表明，我们的组合是非常有效的硬的情况下。
2013-06-08 cs.LO cs.PL
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
Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Model Checking
我们证明了带宽和波前减少算法的适用性静态变量排序。在符号模型检验中，事件局部性在时间和内存使用方面起着重要作用。例如，在Petri网中，事件局部性可以通过依赖矩阵来捕获，其中非零条目指示转换是否修改了位置。事件局部性的质量被表示为称为（加权）事件跨度的度量。矩阵的带宽是一个度量，表示非零元素到对角线的距离。波前是指示矩阵对角线一端上的非零程度的度量。带宽和波前是稀疏矩阵解算器中使用的已充分研究的度量。在这项工作中，我们证明了跨度是有限的两倍的带宽的矩阵。这种观察使得带宽减少算法对于获得良好的可变阶数是有用的。我们解决的一个主要问题是，约简算法只能应用于对称矩阵，而依赖矩阵是不对称的。我们表明，Sloan算法上执行的邻接图的总图给出了最好的变量顺序。实际上，我们证明了我们的工作允许在Boost和ViennaCL中调用标准稀疏矩阵操作，在毫秒内计算非常好的静态变量顺序。未来的工作是有希望的，因为一个全新的频谱更多的现成的算法，包括元启发式的，成为变量排序。
2015-11-27 cs.LO cs.SE
On the size of data structures used in symbolic model checking
Dipartimento di Informatica e Sistemistica（信息与系统学系）；Sapienza Università di Roma（罗马第一大学）
时态逻辑模型检验是一种验证方法，它通过对系统模型的描述，来验证系统中的某些属性（用时态逻辑公式表示）是否成立。它有许多工业应用。为了提高性能，一些工具允许预处理的模型，验证在线的一组属性重用相同的编译模型，我们证明了模型检验问题的复杂性，没有任何预处理或预处理的模型或多项式数据结构中的公式，是相同的。因此，预处理并不总是以指数方式提高性能。符号模型检验算法通过操作状态集来工作，这些状态集通常由BDD表示。已经观察到，BDD的大小可以随着模型和公式的大小的增加而指数地增长。作为一个副作用，我们正式证明，这些BDD的大小的超多项式增加是不可避免的，在最坏的情况下。虽然这种指数增长已被经验观察到，但据我们所知，迄今为止还没有得到一般性的证明。这个结果不仅适用于所有类型的BDD，而不管变量的顺序如何，而且适用于更强大的数据结构，如BED、RBC、MTBDD和ADD。
2010-12-14 cs.AI cs.CC cs.DS
Experiments in Model-Checking Optimistic Replication Algorithms
本文描述了一系列模型检验实验来验证用于支持协同编辑的基于操作转换（OT）方法的乐观复制算法。我们正式定义，使用工具UPPAAL，行为和主要的一致性要求（即收敛性）的协同编辑系统，以及这些系统应该操作的环境的抽象行为。由于数据复制和用户交互的不可预测性，这样的系统有无限多个状态。因此，我们展示了如何利用UPPAAL规约语言的一些功能来减弱严重的状态爆炸问题。提出了两种模型。第一种称为具体模型，它非常接近系统实现，但会遇到严重的状态爆炸。第二种模型称为符号模型，旨在通过延迟编辑操作的有效选择和执行，直到所有站点的符号执行痕迹构建完成，来克服具体模型的局限性。实验结果表明，符号模型允许在空间和时间上的显着增益。使用的符号模型，我们已经能够表明，如果网站的数量超过2，那么收敛性不满足所有OT算法在这里考虑。每个算法都有一个反例。
2008-04-21 cs.LO cs.SC
Experience with Heuristics, Benchmarks & Standards for Cylindrical Algebraic Decomposition
在激发SC广场项目的论文中，[E。Abraham，在符号计算和可满足性检查之间建立桥梁，Proc. ISSAC '15，pp. 1-6，ACM，2015]作者将复杂的逻辑学的使用确定为可满足性检查社区擅长的技术，并且符号计算社区可能从中学习和繁荣。为了开始这个学习过程，我们总结了计算机代数算法柱形代数分解的启发式开发经验。我们还提出并讨论了标准和基准，作为符号计算可以从可满足性检查专业知识中蓬勃发展的另一个领域，注意到这些已被确定为CSA项目中新SC Square社区的初始行动，如[E.~ Abraham等人，SC $^2$：可满足性检查符合符号计算（项目论文）}，智能计算机数学（LNCS 9761），pp. 28- 43，Springer，2015]。
2016-09-29 cs.LO cs.SC
MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the $\exists^*\forall^*$ Fragment
超属性是指多个计算轨迹的属性。这包括许多信息流安全策略，如观察确定性，（广义）不干扰和非推理，以及其他系统属性，如对称性或汉明距离。我们介绍MGHyper，一个自动可满足性检查和模型生成的HyperLTL表示的超属性的工具。与以往的可满足性检查器不同，MGHyper不局限于HyperLTL的可判定$\exists^* \forall^*$片段，而是为全逻辑提供了一个半判定过程。MGHyper的一个重要应用是自动检查不同超性质（以及同一超性质的不同形式化）之间的等价性，并构建反例来反驳某个声称的含义。我们描述了在MGHyper中实现的半决策过程，并报告了从文献中获得的典型超性质和随机生成的HyperLTL公式的实验结果。
2019-03-26 cs.LO
Verifying Reachability Properties in Markov Chains via Incremental Induction
在概率验证和非概率验证之间存在可扩展性差距。概率模型检验工具基于显式引擎或（多端）二元决策图。这些结构在非概率验证领域得到了更可扩展的技术（如IC3）的补充。我们提出了一个符号概率模型检验算法的基础上IC3类增量建设的归纳条款划分的状态空间，交错与增量建设的线性不等式系统。本文比较了我们的实现标准的定量验证的替代方案：我们的实验表明，我们的算法是一个步骤，以更可扩展的符号验证有限状态马尔可夫链中的罕见事件。
2019-09-19 cs.LO
Weakly acyclic diagrams: A data structure for infinite-state symbolic verification
针对OBDDs无法处理无限状态系统的局限，提出弱无环图（WADs）这一OBDDs泛化结构，保留其算法优势并支持无限语言表示，可用于多种无限状态系统的符号模型检测。
2025-02-17 cs.DS cs.LO
Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property
Tel Aviv University（特拉维夫大学）
本文通过符号模型性质证明了扩展分层公式的若干片段的可判定性，允许一种类型有自环函数以放宽量词交替约束。
2026-05-13 cs.LO
Formal Security Analysis of Neural Networks using Symbolic Intervals
Columbia University（哥伦比亚大学）
由于深度神经网络（DNN）在现实世界的安全关键领域（包括自动驾驶汽车和防撞系统）中的部署越来越多，因此正式检查DNN的安全属性（特别是在不同的攻击者能力下）变得至关重要。大多数现有的DNN安全测试技术都试图找到对抗性示例，而没有提供任何关于此类对抗性示例不存在的正式安全保证。最近，有几个项目使用不同类型的可满足性模理论（SMT）求解器来正式检查DNN的安全属性。然而，所有这些方法都受到求解器引起的高开销的限制。在本文中，我们提出了一个新的方向，正式检查DNN的安全属性，而不使用SMT求解器。相反，我们利用区间算术来计算DNN输出的严格边界。我们的方法，不像现有的基于求解器的方法，很容易并行化。我们进一步提出了符号区间分析以及其他几个优化，以尽量减少高估的输出界。我们设计，实现和评估我们的方法作为ReluVal的一部分，正式检查基于Relu的DNN的安全属性的系统。我们广泛的实证结果表明，ReluVal比Reluplex（一种最先进的基于求解器的系统）平均高出200倍。在没有GPU的8核机器上，ReluVal能够在4小时内验证Reluplex认为由于运行超过5天后超时而无法确定的安全属性。我们的实验表明，符号区间分析是一个有前途的新方向，严格分析DNN的不同安全属性。
2018-07-01 cs.AI cs.LO
Neuro Symbolic Reasoning for Planning: Counterexample Guided Inductive Synthesis using Large Language Models and Satisfiability Solving
Florida International University（佛罗里达国际大学）；SRI International（SRI国际（斯坦福国际研究院））；United States Military Academy（美国军事学院（西点军校））；University of Colorado Boulder（科罗拉多大学博尔德分校）；University of Central Florida（中佛罗里达大学）；Vanderbilt University（范德堡大学）
本文提出 LLM 与 SMT 求解器迭代交互的神经符号框架，通过反例反馈修正规划综合结果，并在积木规划任务中验证其可生成可证明正确的解。
2023-09-28 cs.AI cs.LO
Incremental Bounded Model Checking of Artificial Neural Networks in CUDA
Federal University of Amazonas（亚马逊联邦大学）；SIDIA Instituto de Ciência e Tecnologia（SIDIA科学技术研究所）；University of Manchester（曼彻斯特大学）
人工神经网络（ANN）是用于各种应用的强大的计算系统，这是由于其通用性来概括和响应意外的输入/模式。然而，人工神经网络的安全关键系统的实现可能会导致故障，这是很难预测的设计阶段，因为人工神经网络是高度并行的，他们的参数是很难解释。在这里，我们开发并评估了一种基于增量有界模型检验（BMC）的新型符号软件验证框架，以检查多层感知器（MLP）中的对抗性情况和覆盖方法。特别是，我们进一步开发了高效的基于SMT的图形处理单元上下文有界模型（ESBMC-GPU），以确保某些安全属性的可靠性，其中安全关键系统可能会出现故障并做出错误的决策，从而导致不必要的材料损坏甚至危及生命。本文标志着第一个符号验证框架的原因在CUDA实现的人工神经网络。我们的实验结果表明，我们在ESBMC-GPU上实现的方法可以成功地验证人工神经网络的安全属性和覆盖方法，并正确地生成28个MLP对抗案例。
2019-07-30 cs.LG cs.LO cs.NE
Minimal Proof Search for Modal Logic K Model Checking
LAMSADE（拉马萨德实验室）；Université Paris-Dauphine（巴黎第九大学）
大多数模态逻辑，如S5、LTL或ATL，都是模态逻辑K的扩展。虽然LTL和ATL的模型检验问题在过去的几十年里一直是非常活跃的研究领域，但更基本的多智能体模态逻辑K（MMLK）的模型检验问题本身作为完美信息多人游戏的正式框架具有重要的应用。我们提出了最小证明搜索（MPS），努力数为基础的算法解决的模型检验问题MMLK。我们证明了MPS的正确性之外的两个重要性质。MPS证明对于一般的代价定义是代价最小的，MPS是寻找代价最小的证明的最优算法。最优性意味着任何类似的算法要么需要探索比MPS更大或相等的状态空间，要么不能保证在每个输入上找到最小成本的证明。因此，我们的工作涉及A* 和AO* 在启发式搜索，证明数搜索和DFPN+在两个玩家的游戏，并在软件模型检验的反例最小化。
2012-07-10 cs.AI cs.LO
ATL*AS: An Automata-Theoretic Approach and Tool for the Verification of Strategic Abilities in Multi-Agent Systems
本文提出面向无限迹与有限迹语义的 ATL* 符号化模型检测算法，并在 ATL*AS 工具中实现，实验证明其在可扩展性和效率上优于现有方法。
2025-10-21 cs.LO cs.MA
A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking
The Hong Kong University of Science and Technology（香港科学与技术大学）
针对IC3算法在硬件模型检查中归纳泛化策略固定的问题，提出基于机器学习的轻量级框架，利用多臂赌博机算法动态选择策略，经实验验证该方法能有效提升rIC3解决案例数量及PAR-2分数。
2026-07-16 cs.LG cs.LO
OCTAL: Graph Representation Learning for LTL Model Checking
Purdue University（普渡大学）
针对传统符号模型检测的状态空间爆炸问题，提出基于图表示学习的OCTAL框架，将LTL模型检测转化为二分类任务，实现了显著的准确率与最高11倍的整体加速。
2023-08-19 cs.AI cs.LO cs.SE
