Model Checking C++ Programs
在过去的三十年中，系统程序设计语言（如C或C++）中的内存安全问题一直是安全漏洞的重要来源之一。然而，只有少数尝试有限的成功，以应付C++程序验证的复杂性。在这里，我们描述和评估一种新的验证方法的基础上有界模型检验（BMC）和可满足性模理论（SMT），以验证C++程序的形式。我们的验证方法分析有界C++程序的SMT编码到各种复杂的功能，C++程序设计语言提供，如模板，继承，多态性，异常处理，和标准C++库。我们正式这些功能在我们的形式化验证框架内使用一阶逻辑的可判定片段，然后显示如何国家的最先进的SMT求解器可以有效地处理。我们在ESBMC之上实现了我们的验证方法。我们将ESBMC与LLBMC和DIVINE进行比较，它们是直接从LLVM位代码检查C++程序的最先进的验证器。实验结果表明，ESBMC能够处理大范围的C++程序，具有较高的验证正确率。与此同时，与LLBMC和DIVINE工具相比，它减少了验证时间。此外，ESBMC已被应用于电信领域的商业C++应用程序，并成功地检测到算术溢出错误，可能导致安全漏洞。
2021-07-02 cs.SE
SMT-Based Bounded Model Checking of Fixed-Point Digital Controllers
Federal University of Amazonas（亚马孙联邦大学）
本文提出利用基于可满足性模理论的最新有界模型检查器检测数字控制器设计错误，通过球和梁装置实验验证其在发现固定点处理器错误方面的有效性。
2014-03-20 cs.SE cs.SY eess.SY
Early Verification of Legal Compliance via Bounded Satisfiability Checking
本文提出一种基于 SMT 的有界可满足性检查方法，用于在早期需求阶段验证 MFOTL 形式化的法律合规性，并在多个领域案例中证明其能高效判定合规或生成反例。
2023-05-28 cs.SE
Distributed Bounded Model Checking
程序验证是一项耗费大量资源的任务。本文着眼于并行化SMT为基础的自动程序验证，特别是有界模型检查，使其可以分布和执行的机器集群的问题。我们提出了一个算法，动态展开的程序的调用图，并经常分裂它创建子任务，可以并行解决。该算法是自适应的，根据可用资源控制拆分速率，并且还利用来自SMT求解器的信息来拆分搜索中最复杂的地方。我们实现了我们的算法，通过修改CORRAL，微软的静态驱动程序验证器（SDV）使用的验证器，并评估它的一系列硬SDV基准。
2020-05-16 cs.PL cs.SE
IRONPROOF: COBOL-to-Python Transpilation with SMT-Based Equivalence Checking
Ironproof
IRONPROOF是基于SMT等价性检查的COBOL转Python工具，在2345个COBOL文件上验证等价性，独立程序等价率52.6%，可检测溢出，证明仅保证中间表示与Python等价而非COBOL实现等价。
2026-10-09 cs.SE
Quantifying SMT Solver Instability for Formal Verification
St. Olaf College（圣奥拉夫学院）
本文针对形式化验证中SMT求解器的不稳定性问题，采用变异系数量化三个软件领域SMT查询的不稳定性，发现其显著且随查询平均时长增加而上升，提出优化查询结构可缓解不稳定性并提升性能。
2026-10-12 cs.SE
Formal Analysis of Hybrid-Dynamic Timing Behaviors in Cyber-Physical Systems
由于系统和环境中的混合动力学，使用闭环验证来确保信息物理系统（CPS）中的时间行为的正确性具有挑战性。Simulink和Stateflow是基于模型的设计工具，支持各种机制，用于建模和分析实时嵌入式系统的混合动力学。在本文中，我们提出了一种基于SMT的方法，形式化分析的混合动态时序行为的CPS建模在Simulink块和Stateflow状态（S/S）。将层次化互连的S/S扁平化并转换为SMT求解器的输入语言进行形式化验证。提供了一种翻译算法以促进翻译。针对S/S模型的时序约束的形式化验证被简化为对所得到的SMT编码的有效性检查。我们的方法的适用性证明了一个无人水面舰艇的案例研究。
2019-10-31 cs.SE
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
Formal Verification, Engineering and Business Value
如何将模型检验和静态程序分析等自动化验证技术应用于数百万行嵌入式C/C++代码？如何将这种技术包装成软件开发人员和工程师可以使用的方式，他们可能没有形式化验证的背景？以及如何说服企业经理实际支付这样的软件？这项工作解决了其中一些问题。基于我们自己开发和发布Goanna源代码分析器的经验，我们解释了模型检验，静态分析和SMT解决的底层技术，涉及创建工业证明工具的步骤。
2013-01-01 cs.SE
Neurosymbolic Auditing of Natural-Language Software Requirements
Stevens Institute of Technology（史蒂文斯理工学院）
本文提出神经符号方法用于审计自然语言软件需求，通过形式逻辑转换和SMT求解器检测歧义与不一致，提升医疗设备软件需求的严谨性。
2026-05-13 cs.AI cs.SE
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
Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version)
本文提出将外部辅助不变量注入基于 Craig 插值的软件模型检查算法，并在 CPAchecker 中实现，减少插值查询、提升效率且解决了现有工具无法处理的验证任务。
2024-10-25 cs.SE
Constraint-Based Deadlock Checking of High-Level Specifications
在形式化方法的许多应用中，确定没有死锁是很重要的。模型检验用于发现形式化模型中的死锁的使用通常是有限的。在本文中，我们提出了一个基于约束的方法来寻找死锁采用ProB约束求解器。我们提出的一般技术，以及各种改进，必须进行ProB的Prolog内核，如具体化的成员资格和算术约束。这项工作是由一个工业案例研究指导的，博世的一个团队正在对巡航控制系统进行建模。在这个案例研究中，ProB能够快速找到非常大的无死锁约束的反例。在本文中，我们还介绍了这种新技术的其他成功应用。使用SAT和SMT求解器对这些约束的实验迄今为止是不成功的。
2011-09-09 cs.LO cs.PL cs.SE
EquivFusion: Unifying Hardware Equivalence Checking from Algorithms to Netlists via MLIR
National Center of Technology Innovation for EDA（国家集成电路创新中心）；Southeast University（东南大学）；The Chinese University of Hong Kong（香港中文大学）
本文提出EquivFusion工具，通过MLIR统一多模态电路设计的算法与硬件等价性检查，解决软件与硬件之间语义差距的问题。
2026-04-17 cs.AR cs.SE
Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art
属性导向可达性（PDR）是一种基于SAT/SMT的可达性算法，它递增地构造归纳不变量。在成功地应用于硬件模型检验之后，提出了几种适用于软件模型检验的改进方法。我们贡献了一个可复制的和彻底的比较评估的最先进的：我们（1）实现了一个独立的PDR算法，并作为改进，基于PDR的k-induction的不变量生成器，（2）进行了实验研究的最大的公开可用的基准测试集的C验证任务，在其中，我们探索的有效性和效率的软件验证PDR。我们工作的主要贡献是通过提供一个精心设计的参考实现和现有技术的实验评估，为该领域正在进行的研究建立一个可重复的基线。
2020-02-24 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
Software Model Checking via Large-Block Encoding
抽象可达树（ART）的构造和分析是软件验证方法成功的基础。ART表示程序的控制流图的展开。传统上，ART的转换表示程序的单个块，因此，我们称这种方法为单块编码（SBE）。SBE可能会导致大量的程序路径被探索，这构成了效率低下的根本原因。我们提出了一个概括的方法，其中过渡的艺术代表更大的部分程序，我们称之为这种方法的大块编码（LBE）。LBE可以将待探索的路径的数量减少到指数级。在这个框架内，我们还研究了符号表示：对于表示抽象状态，除了在SBE中使用的合取，我们研究了使用任意布尔公式;对于计算抽象后继状态，除了在SBE中使用的笛卡尔谓词抽象，我们研究了使用布尔谓词抽象。新的编码利用了最先进的SMT求解器的效率，它可以象征性地计算抽象的大块后继。我们在基准C程序上的实验表明，大块编码优于单块编码。
2009-04-29 cs.PL cs.SE
NeuroAbs: A Neuro-Symbolic RTL Abstraction Framework for Property Checking Acceleration
The Hong Kong University of Science and Technology (Guangzhou)（香港科技大学（广州））；The Hong Kong University of Science and Technology（香港科技大学）
本文提出NeuroAbs框架，结合LLM与AST实现RTL抽象，通过SMT验证抽象正确性、CEGAR迭代精化，可加速硬件属性检查，解决现有方法人工成本高或灵活性不足的问题。
2026-08-19 cs.AI cs.AR cs.SE
Model Checking Software Programs with First Order Logic Specifications using AIG Solvers
静态验证技术利用布尔公式可满足性求解器（诸如分别对合取范式和一阶逻辑公式进行操作的SAT和SMT求解器）来验证程序。它们强制限制变量范围和执行时间，并将程序及其规范转换为布尔公式。由于以下原因，它们仅限于相对较低复杂性的程序。(1)边界的小幅增加可能会导致转换公式的大小大幅增加。(2)布尔可满足性求解器仅限于使用在公式级别应用的优化。最后，（3）布尔公式通常需要重新生成更高的界限，以确保翻译的正确性。我们提出了一种方法，使用时序电路，布尔公式与记忆元素和层次结构，和时序电路综合和验证框架来验证程序。(1)时序电路比没有存储器元素的布尔公式简洁得多，并且保留了程序的高级结构。(2)将问题编码为时序电路，可以使用许多强大的自动分析技术，这些技术对于其他布尔公式没有对应物。我们的方法需要一个命令式的程序与一阶逻辑规范组成的一个前提条件和一个后置条件对，和一个绑定的程序变量范围，并产生一个时序电路与指定的输出是真的，当程序违反了规范。
2014-09-24 cs.PL cs.SE
Solver-Aided Verification of Policy Compliance in Tool-Augmented LLM Agents
University of Washington（华盛顿大学）
本文提出一种基于SMT求解器的框架，用于确保工具增强大语言模型代理在工具使用上的政策合规性，通过将自然语言政策转化为形式逻辑约束，并在运行时检查工具调用以防止违规。
2026-03-20 cs.AI cs.SE
Jolie Static Type Checker: a prototype
程序源代码正确性的静态验证是软件可靠性的重要内容。软件程序的形式化验证涉及证明程序满足其行为的形式化规范。许多语言同时使用静态和动态类型检查。使用这种方法，静态类型检查器在编译时验证所有可能的内容，并动态检查其余内容。Jolie程序设计语言的当前状态包括动态类型系统。因此，它允许可避免的运行时错误。该语言的静态类型系统已经在纸上正式定义，但还缺乏实现。在本文中，我们描述了一个原型的Jolie静态类型并行计算器（JSTC），它采用了基于SMT求解器的技术。我们描述了背后的理论和实现，以及静态分析的过程。
2017-10-18 cs.PL cs.SE
Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code
KTH Royal Institute of Technology（皇家理工学院）；TRATON AB（特拉顿股份公司）
本文提出了一种用于验证嵌入式汽车C代码非功能需求的合同方法，通过设计通用规则和接口规范语言，结合Frama-C插件实现对控制流和数据流的检查，确保模块调用安全函数并避免未初始化变量。
2026-08-17 cs.PL cs.SE
