SMT-Based Model Checking of Industrial Simulink Models
嵌入式系统的开发需要对模型进行形式化的分析，例如使用MATLAB/Simulink描述的模型。然而，工业模型的日益复杂使得分析变得困难。提出了一种基于SMT求解器的Simulink模型模型检验方法。所提出的方法旨在（1）复杂模型的自动化，高效和可理解的验证，（2）模型的数值精确分析，以及（3）使用SMT求解器（我们使用Z3）演示Simulink模型的分析。它首先将目标模型编码为数学算术和位向量域中的谓词逻辑公式。我们将探讨如何对各种Simulink模块进行精确编码。然后，该方法使用基于k-归纳的算法来验证给定的不变性，该算法提取涉及目标块的子系统并增量地展开执行路径。在实验中，我们将所提出的方法和其他工具应用于一组模型和属性。我们的方法成功地验证了大多数属性，包括那些未验证的其他工具。
2022-06-07 cs.LO
SMT Queries Decomposition and Caching in Semi-Symbolic Model Checking
在半符号（控制-显式数据-符号）模型检验中，状态空间爆炸问题通过位向量理论上的一阶公式表示状态集来解决。在这种模型检验方法中，大部分验证时间都花在SMT求解器上，用于确定量化查询的可满足性，这些量化查询表示符号状态的相等性。在本文中，我们介绍了一个新的计划分解的符号状态，它可以用来显着提高任何半符号模型检查器的性能。使用分解，与原始情况相比，模型检查器可以向求解器发出更简单和更小的查询。一些SMT调用甚至可以完全避免，因为一些简化公式的满足可以从语法上决定。此外，分解允许用于量化公式的高效缓存方案。为了支持我们的理论贡献，我们展示了我们的模型检查器SymDIVINE的性能增益的一组例子，从软件验证比赛。
2017-11-20 cs.LO cs.PL
SMT-based Model Checking for Recursive Programs
提出了一种基于SMT的递归程序安全性验证的符号模型检验算法。该算法是模块化的，并单独分析程序。与其他基于SMT的方法不同，它既保持了程序摘要的“过度近似”，也保持了程序摘要的“欠近似”。欠近似用于分析过程调用，而无需内联。过近似用于阻止不可行的反例和检测收敛到一个证明。我们表明，程序和属性的可判定理论，该算法是保证找到一个反例，如果存在的。然而，效率依赖于用于量词消去（QE）的预言。对于布尔程序，该算法是一个多项式决策过程，匹配最佳BDD算法的最坏情况的界限。对于线性算术（整数和有理数），我们通过“懒惰地”应用QE给出了算法的有效实例。我们使用现有的插值技术来过度近似QE，并引入“基于模型的投影”来欠近似QE。在SV-COMP基准测试上的实验结果表明，该算法在最新水平上有了显著的改进。
2014-05-25 cs.LO
On Neural Network Equivalence Checking using SMT Solvers
Aristotle University of Thessaloniki（塞萨洛尼基亚里士多德大学）；Northeastern University（东北大学）
如果两个预训练的神经网络对相同的输入产生相似的输出，则它们被认为是等效的。神经网络的等价性检查是非常重要的，因为当需要满足额外的要求或解决安全威胁时，其在用等价的组件替换学习使能的组件中的实用性，例如当使用知识蒸馏、对抗训练等时。SMT求解器可以潜在地提供对神经网络等价性检查的问题的解决方案，其将是健全和完整的，但是正如所预期的，任何这样的解决方案都与关于要检查的神经网络的大小的显著限制相关联。这项工作提出了第一个基于SMT的编码的等价性检查问题，探讨其效用和局限性，并提出了未来的研究和改进途径，以实现更可扩展和实际适用的解决方案。我们目前的实验结果，揭示了上述问题，不同类型的神经网络模型（分类器和回归网络）和等价性标准，对一个通用的和应用程序无关的等价性检查方法。
2022-03-22 cs.AI cs.LG cs.LO
A Polyhedral Abstraction for Petri nets and its Application to SMT-Based Model Checking
本文提出一种基于多面体抽象的Petri网约简方法，结合SMT模型检验器，通过等价关系保证正确性，并在SMPT工具中实现BMC和PDR，实验验证其有效性。
2022-10-11 cs.LO
QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking
University of Manchester（曼彻斯特大学）；University of Amazonas（亚马逊大学）
QNNVerifier是第一个用于验证神经网络实现的开源工具，它考虑了操作数的有限字长（即量化）。新的支持量化是通过采用最先进的软件模型检验（SMC）技术。它将神经网络的实现转化为基于可满足性模理论（SMT）的一阶逻辑的可判定片段。固定和浮点运算的影响表示通过直接实现给定的硬件确定的精度。此外，QNNVerifier允许指定定制的安全属性，并使用不同的验证策略（增量和k-归纳）和SMT求解器验证生成的模型。最后，QNNVerifier是第一个通过区间分析和非线性激活函数的离散化结合不变推理的工具，以数量级加速神经网络的验证。有关QNNVerifier的视频演示，请访问https://youtu.be/7jMgOL41zTY
2021-11-25 cs.AI cs.LG cs.LO
Automatic Abstraction in SMT-Based Unbounded Software Model Checking
基于欠近似和SMT求解器的软件模型检查器在验证安全性（即可达性）属性方面非常成功。它们结合了两个关键思想-（a）“具体性”：在一个下近似的反例是一个反例，以及在原来的程序，和（b）“泛化”：一个下近似的安全性证明，由SMT求解器，是可推广到原程序的安全性证明。在本文中，我们提出了一个“自动抽象”与近似驱动的框架。我们探讨了两种迭代的方法来获得和细化抽象-“基于证明”和“基于反例”-并展示了它们如何组合成一个统一的算法。据我们所知，这是基于证明的抽象的第一个应用程序，主要用于验证硬件，软件验证。我们已经实现了一个原型的框架使用Z3，并评估它的许多基准软件验证比赛。我们的实验表明，我们的组合是非常有效的硬的情况下。
2013-06-08 cs.LO cs.PL
Abstraction and Acceleration in SMT-based Model-Checking for Array Programs
抽象（以其各种形式）是模型检验中一种强大的既定技术;然而，当涉及无界数据结构时，它并不总是以令人满意的方式处理发散现象。加速是一种广泛应用的避免发散的方法，但它主要应用于整数规划。本文讨论了无界数组的加速转换关系问题，最终目标是避免抽象程序可达性分析过程中的发散。为此，我们首先设计了一种格式来计算在这个域中的加速度，然后我们展示了如何适应所谓的“单调抽象”技术，以有效地处理复杂的公式与嵌套的量词所产生的加速预处理。值得注意的是，我们的技术可以很容易地插入到抽象/细化循环，并大大有助于避免发散：与MCMT模型检查器进行的实验证明了我们的方法对具有无界数组的程序的有效性，如果单独应用加速和抽象/细化技术，则会失败。
2013-10-03 cs.LO
Global Guidance for Local Generalization in Model Checking
基于SMT的模型检测器，特别是IC 3型的模型检测器，是目前验证无限状态系统的最有效的技术。他们通过局部推理系统的过渡关系的单步的来推断全局归纳不变量，同时采用基于SMT的程序，如插值，以减轻局部推理的局限性，并允许更好的泛化。不幸的是，这些缓解措施干扰了模型检验与底层SMT求解器的并行性，对模型检验的稳定性产生了负面影响。在本文中，我们建议以系统的方式解决局部性的局限性。我们引入明确的全球指导到IC 3风格的算法进行局部推理。为此，我们扩展了SMT-IC 3范式与三个新的规则，旨在减轻故障的根本来源，源于本地。我们将这些规则实例化为线性代数算法的理论，并在Z3中的SPACER求解器上实现它们。我们的实证结果表明，GSPACER，扩展与全球指导的空间，是显着更有效的空间和唯一的全球推理，而且，是不敏感的插值。
2020-05-27 cs.FL cs.LO
Invariant Checking for SMT-based Systems with Quantifiers
针对由 SMT 理论与量词定义的符号迁移系统，论文提出两种结合 IC3、隐式谓词抽象及下近似推广的全称归纳不变式检查算法，实验显示其统一处理能力和性能均具竞争力。
2024-02-29 cs.LO
LTL Model-Checking for Dynamic Pushdown Networks Communicating via Locks
动态下推网络（Dynamic Pushdown Network，DPN）是一组下推系统（Pushdown Systems，PDS），其中每个进程都可以动态地创建新的PDS实例。DPN是具有（可能是递归的）过程调用和线程创建的多线程程序的自然模型。使用锁扩展DPN允许进程彼此同步。因此，带锁的DPN是一种很好的形式主义，可以对通过锁进行同步的多线程程序进行建模。因此，为带锁的DPN提供模型检验算法是很重要的。在这项工作中，我们认为模型检验的DPN与锁对单索引的LTL属性的形式V fi s. t。fi是在PDS i上解释的LTL公式。我们考虑模型检验问题w.r.t.简单赋值（即，配置是否满足原子命题仅取决于其控制位置和持有的锁）和w.r.t.定期评估（即，满足原子命题的配置集合是配置的规则集合）。我们证明了这些模型检验问题是可判定的。
2016-10-11 cs.LO cs.PL cs.SE
Interpolation and Model Checking for Nonlinear Arithmetic
提出了一种新的基于模型的可满足性模理论插值方法。该过程使用了一种新的与SMT求解器的交互模式，我们称之为求解模模型。这要么将给定的部分模型扩展为一组断言的完整模型，要么在不存在解决方案时返回解释（模型插值）。这种交互模式非常适合SMT的模型构建可满足性（MCSAT）框架。我们用它来开发任何MCSAT支持的理论的插值程序。特别是，这种方法导致了一个有效的非线性实算术插值程序。我们评估新的程序，将其集成到一个模型检查器，并将其与最先进的非线性算法的模型检查工具进行比较。
2021-06-08 cs.LO cs.PL cs.SC
A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
LIPN CNRS UMR 7030 Université Sorbonne Paris Nord（巴黎北大学国家科学研究中心联合研究实验室）；Pohang University of Science and Technology（韩国科学技术院）；University of Oslo（奥斯陆大学）
本文提出了一种用于参数时间Petri网的形式化分析与参数综合框架，利用重写逻辑与SMT求解器实现精确语义分析，通过符号可达性方法实现参数综合，实验表明方法在多个方面优于现有工具。
2024-09-12 cs.LO
Formal Verification of Safety Properties Using Interpolation and k-induction
本技术报告介绍了使用SAT/SMT求解器的两种符号模型检验算法的实现，即基于插值的模型检验和基于k-归纳的模型检验。并对这两种模型检验算法进行了比较分析。
2022-07-04 cs.LO
Using SMT Solvers to Validate Models for AI Problems
Alexandru Ioan Cuza University of Iaşi（雅西亚历山德鲁·伊万·库扎大学）
人工智能问题，从规划/调度到游戏控制，包括一个重要的关键步骤：描述一个模型，该模型准确定义了问题所需的数据，要求，允许的过渡和既定的目标。模型失败的方式有很多，并且通常会导致搜索策略无法提供快速、最佳甚至任何解决方案。本文提出使用SMT（可满足性模理论）求解器，如Z3，来检查模型的有效性。我们提出两个测试：检查最终（目标）状态是否存在于模型描述的问题空间中，并检查所描述的转换是否可以提供从所识别的初始状态到任何目标状态的路径（意味着已经找到解决方案）。使用SMT求解器进行AI模型检验的优点在于，它们替代了实际的搜索策略，并且它们处理模型的抽象表示，即一组逻辑公式。在抽象层面上进行推理并不像探索整个解决方案空间那样昂贵。SMT求解器使用有效的决策过程，为与AI模型相对应的逻辑公式提供证明。Z3最近添加的一个功能允许我们将转换序列描述为递归函数，因此我们可以检查是否可以在定义的模型中找到解决方案。
2019-03-22 cs.AI cs.LO
BPPChecker: An SMT-based Model Checker on Basic Parallel Processes(Full Version)
并发程序的程序验证是一个很大的挑战，由于一般的不可判定的结果。Petri网及其扩展在大多数工作中使用。然而，现有的基于Petri网的验证器很难是完整的和有效的。基本并行进程（BPP）作为Petri网的一个子类，可以作为描述和验证并发程序的模型，具有较低的复杂度。我们提出并实现了BPP的，第一个模型检查器，用于验证一个子类的CTL BPP。针对BPP的模型检验问题，提出了基于约束的算法，并用SMT求解器Z3处理公式。对于EF算子，我们将EF公式的模型检验归结为存在Presburger公式的可满足性问题。对于EG算子，我们给出了k步有界语义，并将EG公式的模型检验问题归结为线性整数运算的可满足性问题。此外，我们给演员通信系统（ACS）的过近似BPP的语义和评估BPP的演员通信系统从真正的Erlang程序生成。实验结果表明，BPPPERT在一系列Erlang程序的分支时间属性验证问题上比现有工具有更高的效率。
2021-10-25 cs.FL cs.LO
Model Checking for Rectangular Hybrid Systems: A Quantified Encoding Approach
可满足性模理论（SMT）求解器已经成功地应用于解决形式化验证中的许多问题，例如从集成电路到信息物理系统的许多类系统的有界模型检验（BMC）。通常，BMC是通过检查一个可能很长但没有量词的公式的可满足性来执行的。然而，BMC问题可以自然地编码为BMC步骤数量的量化公式。在这种方法中，我们然后使用决策程序支持量词来检查这些量化公式的可满足性。该方法先前已被应用于使用量化布尔公式（QBF）编码来执行用于纯离散系统的BMC，然后使用QBF求解器来释放QBF检查。在本文中，我们提出了一个新的量化编码的BMC矩形混合自动机（RHA），这需要使用更一般的逻辑，由于实（密集）时间和实值状态变量建模连续状态。我们已经实现了一个初步的实验原型的方法，使用HyST模型转换工具生成量化BMC（QBMC）查询的Z3 SMT求解器。我们描述了几个时间和混合自动机的基准，如费舍尔和林奇-斯考特互斥算法的实验结果。我们将我们的方法与无量化器的BMC方法进行比较，例如使用dReal SMT求解器的dReach工具中的方法，以及使用MathSAT SMT求解器构建在nuXmv之上的HyComp工具。基于我们有前途的实验结果，QBMC可能在未来是一个有效的和可扩展的分析方法RHA和其他类的混合自动机的进一步改进，在SMT求解器，如Z3的量词处理。
2022-07-14 cs.FL cs.LO cs.SC
Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN (Extended Version)
我们提出了DAB --BPMN的一个数据感知扩展，该过程在案例和持久性数据上运行（分为一个称为目录的只读数据库和一个称为存储库的读写数据库）。该模型的表达能力和支持参数化验证的安全属性的可能性之间的权衡。具体而言，从文献中的灵感验证的工件系统，我们研究的安全属性检查无关的只读目录的内容，并接受潜在的存在无限的许多元组的目录和存储库中的验证问题。我们解决这样的问题，使用一个基于数组的向后可达性过程完全实现MCMT-一个国家的最先进的基于数组的SMT模型检查。值得注意的是，我们证明了该程序是健全的和完整的检查安全的DAB，并挑选出额外的条件，保证其终止，反过来，检查安全的可判定性。
2019-06-24 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
Bounded Model Checking of C++ Programs Based on the Qt Framework (extended version)
嵌入式系统的软件开发过程越来越快，这通常会导致相关复杂性的增加。因此，消费电子公司通常在快速和自动验证过程中投入大量资源，以创建强大的系统并降低产品召回率。正因为如此，本文提出了一个简化版本的Qt框架，这是集成到有效的基于SMT的有界模型检验工具，以验证实际应用程序，使用所提到的框架。本文提出的方法提出了一个成功率为94.45%，为开发的测试套件。
2015-09-05 cs.LO cs.SE
Exploiting Hierarchy in the Abstraction-Based Verification of Statecharts Using SMT Solvers
在基于状态的系统设计中，状态图经常被用作建模形式。形式化验证技术也经常用于证明系统行为的某些属性。形式化验证最有效的技术之一是反例引导的抽象精化（CEGAR），它通过自动构建和精化抽象来降低系统的复杂性。在我们的论文中，我们提出了一种新的适应CEGAR方法层次状态图模型。首先，我们引入一个编码的状态图的逻辑公式，保留有关的状态层次结构的信息。基于这种编码，我们提出了抽象和细化技术，这些技术利用状态图的分层结构，并处理模型中的变量。编码使我们能够使用SMT求解器的系统的探索和验证的抽象模型，也包括有界模型检验。我们证明了我们的抽象技术的适用性和效率与测量行业的动机的例子。
2017-03-21 cs.LO cs.SE
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
Improved Bounded Model Checking of Timed Automata
时间自动机（TA）是一个非常流行的建模形式主义的时间敏感的属性。一个常见的任务是验证TA的网络是否满足给定的属性，通常用线性时态逻辑（LTL）或时间计算树逻辑（TCTL）的子集表示。在本文中，我们建立在TACK有界模型检查TA，它支持基于信号的语义TA和更丰富的度量区间时态逻辑（MITL）。TACK将TA网络和属性编码为LTL的变体，即时钟约束LTL（CLTLoc）。产生的CLTLoc公式然后可以通过诸如Zot的工具求解，该工具将CLTLoc属性转换为可满足性模理论（SMT）求解器的输入逻辑。我们提出了一种新的方法，保留TACK的MITL属性的编码，同时直接到SMT求解器语言编码的TA网络，利用BitVector逻辑和逻辑的实算术。我们还介绍了几个优化，使我们能够显着优于CLTLoc编码在许多实际情况下。
2021-04-26 cs.LO
HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
HornStr 是首个将正则模型检验的不变式合成转化为字符串上的约束 Horn 子句问题的求解器，支持 L* 和基于 SAT 的自动机学习，并自动验证 MU 谜题，生成超 30000 个新基准。
2025-05-23 cs.FL cs.LO
On using floating-point computations to help an exact linear arithmetic decision procedure
CNRS / VERIMAG（法国国家科学研究中心 / VERIMAG）
提出一种可选的预处理阶段，通过浮点计算加速基于单纯形法的SMT求解器，保持正确性和完备性，实验表明该方法能显著提升效率。
2009-04-22 cs.LO cs.NA math.NA
JBMC: A Bounded Model Checking Tool for Java Bytecode
JBMC是一个开源的基于SAT和SMT的有界模型检验工具，用于验证Java字节码。JBMC依赖于Java库的操作模型，它保守地近似于它们的语义，以验证断言违规，数组越界，意外的算术溢出以及Java字节码中的其他类型的功能和运行时错误。如果状态空间的深度上界是已知的，则JBMC可以用于伪造属性或证明程序正确性。JBMC的实际应用包括但不限于错误发现、属性检查、测试输入生成、安全漏洞检测和程序合成。在这里，我们提供了一个详细的描述JBMC的架构和它的功能，包括深入讨论其背景理论和底层技术，包括一个国家的最先进的字符串求解器，以确保Java字节码的安全性和安全性。
2023-02-05 cs.LO cs.PL cs.SE
Using Bounded Model Checking to Focus Fixpoint Iterations
在通过抽象解释的静态分析中，两个经典的不精确性来源是加宽和合并操作。合并操作可以通过区分路径来完成，就像在跟踪分区中一样，代价是枚举指数数量的路径。在这篇文章中，我们描述了如何避免这种系统的探索，集中在一个单一的路径，指定的SMT解决。我们的方法与加速技术结合得很好，因此在某些情况下也可以消除加宽。我们说明了它的公知的凸多面体域。
2011-06-14 cs.LO cs.PL
Constraint-Based Deadlock Checking of High-Level Specifications
在形式化方法的许多应用中，确定没有死锁是很重要的。模型检验用于发现形式化模型中的死锁的使用通常是有限的。在本文中，我们提出了一个基于约束的方法来寻找死锁采用ProB约束求解器。我们提出的一般技术，以及各种改进，必须进行ProB的Prolog内核，如具体化的成员资格和算术约束。这项工作是由一个工业案例研究指导的，博世的一个团队正在对巡航控制系统进行建模。在这个案例研究中，ProB能够快速找到非常大的无死锁约束的反例。在本文中，我们还介绍了这种新技术的其他成功应用。使用SAT和SMT求解器对这些约束的实验迄今为止是不成功的。
2011-09-09 cs.LO cs.PL cs.SE
SMT-based Induction Methods for Timed Systems
在验证方法的许多应用中，对时间相关方面进行建模是很重要的。对于精确的结果，有必要将时间解释为密集域，例如使用时间自动机作为形式主义，即使系统产生的无限状态空间对验证方法具有挑战性。此外，完全符号化处理的状态空间的定时相关和非定时相关的元素似乎提供了一个有吸引力的方法，模型检验定时系统与大量的非确定性。本文提出了一种基于SMT的定时系统扩展的IC 3算法，一种新的，高效的，完整的验证方法，基于SAT的非定时系统。在扩展的IC 3算法中，对时间系统的无限状态空间的处理是基于对时间系统的区域抽象进行适当的调整。此外，$k$ -感应，另一个符号验证方法的离散时间系统，以类似的方式扩展到支持定时系统。这两种新的方法进行评估和实验比较，使用原来的离散时间IC 3算法的基于布尔化的验证方法。
2012-04-25 cs.LO
DRAT-based Bit-Vector Proofs in CVC4
用于固定大小位向量理论的许多最先进的可满足性模理论（SMT）求解器采用称为位爆破的方法，其中给定公式被转换成布尔可满足性（SAT）问题并委托给SAT求解器。因此，在SMT求解器中生成位向量证明需要将SAT证明合并到其证明基础结构中。在本文中，我们描述了三种方法，用于将DRAT证明由现成的SAT求解器生成到SMT求解器CVC 4的证明基础设施中，并探索它们的优点和缺点。我们使用cryptominisat作为其比特爆破引擎的SAT后端实现了所有三种方法，并在校对生产和校对方面评估了性能。
2019-07-02 cs.LO
Integrating Loop Acceleration into Bounded Model Checking
本文将循环加速技术动态集成到基于SMT的有界模型检测中，通过添加捷径和阻塞子句，既能快速发现深层反例，又能在BMC发散时证明安全性，实验表明其在证明不安全性方面具有竞争力。
2024-08-09 cs.LO
Transformation von Scade-Modellen zur SMT-basierten Verifikation
在这项工作中，我们开发了一个全自动的验证程序的安全性能的SCADE程序。我们将每个这样的程序转换为SMT实例（可满足性模理论），并将其提供给求解器。我们的目标是拥有一个可公开访问的实验平台，用于验证Scade程序。SMT的选择取决于它提供了比命题逻辑更多的表达逻辑，但它们的求解器已经被证明表现得非常好。SMT逻辑的表达能力使我们能够实现符号化的模型检验，从而避免了在验证过程中扩展模型的完整状态空间。为了降低复杂度，我们分两步将Scade程序转换为SMT实例。首先，它们被简化为同步数据流语言Lama的程序。这种语言的语义比Scade简单，同时仍然保留了一些程序员的抽象。接下来，我们解释这样一个喇嘛程序作为一个系统的量词自由的一阶公式。Lama中剩下的抽象可以用来简化这些系统。这反过来又可以加快核查进程，使更多的财产可以核查。我们使用Haskell在一个软件中成功地实现了这些转换。通过将该软件与Scade套件附带的现有验证软件“Scade Design Verifier”进行比较，得出了这项工作的结论。
2014-03-11 cs.LO
Constraint LTL Satisfiability Checking without Automata
本文提出了一种新的方法来判定用线性时态逻辑语言写的带有将来和过去算子的公式和属于约束系统D的原子公式的可满足性（简称CLTLB（D））。该技术基于有界可满足性的概念，并将CLTLB（D）公式编码为QF-EUD，结合了无量词等式理论和D.类似于标准LTL，其中有界模型检查和SAT求解器可以用作自动机理论方法的模型检查的替代方案，我们的方法允许用户通过SMT求解技术来解决CLTLB（D）公式的可满足性问题，而不是通过检查合适的自动机A_A的语言的空性。该技术是有效的，并已在我们的Zot形式化验证工具中实现。
2014-02-11 cs.LO
Synthesizing Update Schedules with Game-Based Extension of Bounded Model Checking
Carl von Ossietzky Universität Oldenburg（奥尔登堡卡尔·冯·奥西茨基大学）
针对安全关键系统无中断安全软件更新的难题，提出将系统与更新交互建模为双人时间博弈、用有界SMT编码合成全局固定更新调度的方法，经自动驾驶轨迹规划器示例验证可保障所有可允许执行下的安全部署。
2026-09-28 cs.GT cs.LO
Bounded Model Checking of an MITL Fragment for Timed Automata
时间自动机（TA）是一种常见的建模时间系统的形式。有界模型检验（BMC）是一种使用SAT或SMT求解器搜索违反属性的运行的验证方法。MITL是线性时间逻辑LTL的实时扩展。最初，MITL被定义为非重叠时间间隔的轨迹，而不是“超密集”时间轨迹，允许时间间隔重叠在单个点上，这些点被当今常见的时间自动机语义所采用。在本文中，我们扩展的MITL片段的语义超密集的时间轨迹，并设计了一个有界的模型检验编码的片段。我们证明了正确性和完整性的意义上说，使用一个足够大的范围内的反例，任何给定的非控股property.We可以找到实现建议的有界模型检验方法和实验研究的效率和可扩展性的实现。
2013-04-26 cs.LO
Refining Trace Abstraction using Abstract Interpretation
众所周知，当抽象精化过程没有导出循环不变量时，软件模型检验中的CEGAR循环就会发散。基于SMT求解器的抽象细化过程被应用于迹线，即，程序的一种限制形式（没有循环）。在本文中，我们提出了一个新的抽象细化过程，旨在尽可能地规避这种限制。我们将抽象解释应用于我们从给定的跟踪中导出的程序。如果程序包含一个循环，我们保证得到一个循环不变量。我们只在抽象解释返回不确定答案的情况下调用SMT求解器。也就是说，这个想法是使用抽象解释和SMT求解器串联。在痕迹提取设置的实验评估表明，这一想法的实际潜力。
2017-02-08 cs.LO
Formal verification of octorotor flight envelope using barrier functions and SMT solving
介绍了一种八旋翼平台飞行控制器安全性的形式化验证方法。我们的方法涉及到八旋翼的状态空间，被认为是安全的，并可以被证明是不变的动态区域。具体地说，指数障碍函数被用来构建候选不变区域附近的期望的命令状态。使用dReal SMT求解器自动发现这些区域不变的证据，从而确保八旋翼的精确命令跟踪在一定的误差范围内。转子故障，其中转子推力成为固定值卡住被认为是通过一个伪逆控制分配器和占。在dReal中通过检查分配器所需的推力是否超过转子的能力来验证控制分配器的安全性。我们应用我们的方法在一个特定的八旋翼的例子，并验证所需的命令跟踪性能的控制器在正常条件下，转子故障的各种组合。
2021-07-01 cs.LO cs.SY eess.SY
Bounded Quantifier Instantiation for Checking Inductive Invariants
本文提出有界视界量词实例化方法，限制实例化项深度以保证SMT求解器终止，能有效检查归纳不变量，且界限1时可自动模拟插桩，无需修改代码。
2019-08-20 cs.LO cs.PL
Refinement Reflection: Complete Verification with SMT
我们介绍了精化反射，一个新的框架，用于建立基于SMT的演绎验证。关键思想是将实现用户定义函数的代码反映到函数的（输出）细化类型中。因此，在使用函数时，函数定义以允许可判定验证的精确方式在SMT逻辑中实例化。反射允许用户通过使用模式匹配和递归来编写其他程序来编写程序的等式证明，以执行大小写分解和归纳。因此，通过命题作为类型的原则，我们表明，反射允许规范的任意功能的正确性属性。最后，我们介绍了一个证明搜索算法，称为证明逻辑评估，使用技术从模型检验和抽象的解释，完全自动化的等式推理。我们已经在Liquid Haskell中实现了反射，并使用它来验证Monoid，Applicationative，Functor和Monad类型类的广泛使用的实例实际上满足使客户端安全所需的关键代数定律，并使用反射构建了第一个库，该库实际验证了关于关联性和排序的假设，这些假设对于安全的确定性并行性至关重要。
2017-11-09 cs.LO cs.PL
Formal Modeling and SMT-Based Parameterized Verification of Multi-Case Data-Aware BPMN
我们提出了DAB --BPMN事实标准的一个数据感知扩展，它具有对case和持久数据进行操作的能力（分为只读目录和读写存储库），并在表达能力和支持安全属性的参数化验证的可能性之间进行平衡。特别是，我们从工件系统验证的文献中获得灵感，并且考虑其中与只读目录的内容无关地检查安全属性的验证问题，可能考虑目录和储存库中的活动情况和元组的无限数量。这些问题的解决使用完全实现的基于阵列的向后可达性技术属于良好的SMT模型检验的传统。我们还确定了相关类的DAB的MCMT阵列为基础的模型检查器中实现的向后可达性程序是健全和完整的，然后进一步加强这些类，以确保终止。
2019-06-20 cs.LO
Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses
University of Trento（特伦托大学）；University of Freiburg（弗赖堡大学）
本文提出两种新型求解器，结合CDCL与时间顺序回溯，实现高效且不相交的枚举。通过改进的implicant shrinking算法减少部分赋值数量，提升搜索效率，并在投影枚举和SMT推理中表现优异。
2024-11-21 cs.LO
A CDCL-style calculus for solving non-linear constraints
在本文中，我们提出了一种新的方法来检查实数上的非线性约束的可满足性，称为ksmt。该程序是基于CDCL风格的演算冲突解决，使用符号和数值方法的组合。为了处理冲突情况下的非线性组件，我们使用数字构造的限制线性化。这种方法涵盖了大量的可计算的非线性实函数，如多项式，有理或三角函数和超越。几个非线性SMT-LIB的例子和结果进行了比较，与国家的最先进的SMT求解器的原型实现进行了评估。
2019-07-05 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
CTL* model checking for data-aware dynamic systems with arithmetic
复杂动态系统的分析是形式化方法和人工智能的核心研究课题，系统与数据的组合建模在业务流程管理等应用中越来越重要。此外，流程挖掘技术现在被用来自动地从事件数据中挖掘流程模型，通常没有正确性保证。因此，需要验证技术的线性和分支时间属性，以确保所需的行为。在这里，我们考虑数据感知的动态系统与算术（DDSAs），这构成了一个简洁的，但表达形式主义的过渡系统与线性算术后卫。我们提出了一个CTL* 模型检验程序DDSAs依赖于一个有限状态的抽象，通过一组公式，捕捉变量配置。线性时间验证被证明是可判定的，在特定类别的DDSAs的约束语言或控制流被适当地限制。我们调查了几个这些限制的情况下，CTL*，积极和消极的结果：CTL* 验证被证明是可判定的单调性和整数周期性约束系统，但不可判定的反馈自由和有界回看系统。为了证明我们的方法的可行性，我们实现了它在基于SMT的原型ADA，显示出许多实际的业务流程模型可以有效地分析。
2022-05-18 cs.LO
Bounded Model Checking for Unbounded Client Server Systems
IIT Dharwad（印度理工学院达瓦德分校）；NIT Calicut（卡尔库特国立理工学院）
本文提出了一种新的计数逻辑和二维有界模型检查策略，用于验证具有无限客户端的客户端-服务器系统。
2026-02-18 cs.LO
Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
我们提出了一个健全的和完整的方法来验证随机调度下的复制系统的定性活性性质。这些系统由有限状态程序组成，由未知数量的不可区分的代理执行，其中下一个采取行动的代理由随机实验的结果决定。我们表明，如果这样一个系统的一个属性，那么总是有一个证人的Presburger阶段图的形状：一个有限的图形，其节点是Presburger定义的配置集。由于验证问题（非初等）的复杂性很高，我们引入了一个不完整的过程，用于构建Presburger阶段图，并在SMT求解器上实现它。该程序广泛使用了良好的准序理论，以及Petri网和向量加法系统的结构理论。我们将我们的结果应用到一组基准，特别是大量的人口协议，分布式计算模型广泛研究的分布式计算社区。
2020-07-02 cs.DC cs.LO
Technical Report: Exploring Automatic Model-Checking of the Ethereum specification
本研究针对以太坊3SF共识协议的可问责安全性，基于其Python规范用TLA+形式化并结合多层手动抽象，通过Apalache等工具实现小规模实例的穷举验证，未发现安全违规，证明了手动抽象对模型检测效率的提升作用。
2025-01-16 cs.DC 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
Verification of Data-Aware Processes via Array-Based Systems (Extended Version)
我们研究验证的一个一般模型的工件为中心的系统，以评估（参数化）的安全属性无关的初始数据库实例。我们认为这样的工件系统基于数组的系统，这使我们能够检查安全性，通过适应向后可达性，建立了第一次符合模型检验的基础上满意度模理论（SMT）。要做到这一点，我们利用模型理论的机器模型完成，这令人惊讶地证明是一个有效的工具，验证关系系统，并代表了本文的主要原始贡献。这样，我们追求双重目的。一方面，我们重建（限于安全性）的本质，在文献中获得的一些重要的可判定性结果的神器为中心的系统，我们设计了一个真正新颖的类的可判定的情况下。另一方面，我们能够在实现中利用SMT技术，建立在著名的MCMT模型检查器的基于阵列的系统，并扩展它，使我们所有的基础结果完全可操作。
2019-02-27 cs.LO
A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators
Politecnico di Milano（米兰理工大学）；TU Wien（维也纳工业大学）
针对信息物理系统中带界时间算子的离散时间信号时序逻辑（STL）的可满足性检验需求，提出一种利用时间区间冗余加速的树形单次表算法，可拓展用于多种STL相关验证任务，性能优于现有最优编码方法。
2025-07-29 cs.LO
Tarmo: A Framework for Parallelized Bounded Model Checking
本文研究了共享内存环境和工作站集群环境下的有界模型检验（BMC）并行化方法。我们提出了一个通用的框架，并行BMC命名为Tarmo。我们的框架可以与BMC的任何增量SAT编码一起使用，但对于本文中的结果，我们仅使用当前最先进的完整PLTL编码。使用这种编码允许我们检查安全性和活性属性，这与早期分发BMC时仅限于安全属性的工作相反。尽管我们的重点是BMC后，它已被翻译成SAT，现有的分布式SAT求解器并不适合我们的应用程序。这是因为解决BMC问题不是解决一组独立的SAT实例，而是解决多个相关的SAT实例，增量编码，其中每个实例的可满足性对应于特定长度的反例的存在。我们的框架包括一个通用的共享子句数据库的架构，允许SAT求解线程之间轻松共享子句解决各种这样的实例。我们提出了广泛的实验结果与我们的Tarmo实现的多个变体。我们的共享内存变体比传统的单线程方法具有更好的性能，这是许多用户可以受益于多核和多处理器技术的广泛应用的结果。此外，我们证明了我们的框架可以部署在一个典型的工作站集群，其中几个多核机器通过网络连接。
2009-12-13 cs.DC cs.LO
Bounded Satisfiability for PCTL
马尔可夫链的模型检验PCTL是多项式时间可判定的，但PCTL可满足性的判定及其有限模型性质是一个长期存在的问题。虽然一般的可满足性是一个有趣的挑战，从纯理论的角度来看，我们认为，一般的解决方案不会感兴趣的从业者：这样的解决方案可能太大，是可实现的，甚至是无限的。受有界合成技术的启发，我们转向寻求有界大小的模型的更多应用问题：我们将搜索限制在可实现的-因此相当简单的-模型。我们提出了一个程序来决定是否一个给定的PCTL公式有一个可实现的模型，减少到SMT问题。我们已经实现了我们的技术，并发现它们可以应用于健全检查的实际问题-一个程序，允许系统设计人员检查他们的公式是否有一个意外的小模型。
2012-03-30 cs.FL cs.LO
Proceedings of the Third International Workshop on Verification and Program Transformation
本卷包含2015年4月11日在英国伦敦举行的第三届验证和程序转换国际研讨会（VPT 2015）上发表的论文。讲习班的前两届讲习班分别于2013年在圣彼得堡（俄罗斯）和2014年在维也纳（奥地利）举行。这些论文表明，在程序转换领域中开发的方法和工具，如部分求值和折叠/展开转换，以及超级编译，可以应用于软件系统的验证。他们还展示了一些程序验证方法，如模型检验技术，抽象解释，SAT和SMT解决，自动定理证明，可以用来增强程序转换技术，从而使这些技术在实践中更强大和有用。
2015-12-06 cs.LO cs.PL cs.SE
ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification
The University of Manchester（曼彻斯特大学）；Federal University of Amazonas (UFAM)（亚马孙联邦大学）
本文综述了ESBMC从研究原型发展为工业级形式化验证平台的过程，涵盖其技术演进、语言支持扩展、与LLM及AI代理的集成，并总结了其获奖、经济影响及未来挑战。
2026-05-30 cs.LO cs.SE
