Verifying Fixed-Point Digital Filters using SMT-Based Bounded Model Checking
在基于定点运算的处理器中实现数字滤波器会导致与有限字长相关的问题。特别地，在这样的滤波器中的信号的处理可以产生由在累加加法和乘法运算期间的量化和舍入效应引起的溢出和不想要的噪声。在本文中，我们描述了一种新的方法来验证数字滤波器使用现成的有界模型检查器称为ESBMC，它支持完整的C/C++，是基于可满足性模理论求解器。特别是，我们能够验证溢出的发生，极限环，和时间约束的基础上实现的离散时间模型在C。实验表明，该方法可以用来验证数字滤波器定点实现中的潜在问题，从而可以有效地发现现实的设计错误。
2013-07-23 cs.LO cs.SE
A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification
Technology Innovation Institute (TII)（技术创新研究所（TII））；University of Manchester（曼彻斯特大学）
本文提出ESBMC-AI框架，将大语言模型与有界模型检测相结合，自动检测并修复C程序中的缓冲区溢出、算术溢出等漏洞，并在50,000个C程序上验证了其高精度修复能力。
2024-06-27 cs.AI cs.FL cs.LG
Bounded Model Checking of Multi-threaded Software using SMT solvers
从单核处理器到多核处理器的过渡使得多线程软件成为计算机辅助验证的一个重要课题。在这里，我们描述和评估的ESBMC模型检查器的扩展，以支持验证多线程软件共享的变量和锁使用有界模型检验（BMC）的基础上可满足性模理论（SMT）。我们描述了三种方法来模型检查多线程软件和我们的建模的同步原语的Pthread库。在惰性方法中，我们生成所有可能的交织，并分别对每个交织调用BMC过程，直到我们找到一个bug，或者系统地探索了所有交织。在时间表记录方法中，我们将所有可能的交织编码成一个单一的公式，然后利用SMT求解器的高速。在欠近似加宽方法中，我们通过从SMT求解器生成的不可满足性证明中提取状态变量和交织的数量来减少状态空间。在所有这三种方法中，我们都使用了部分降阶（POR）技术来减少交织的数量。实验表明，我们的方法可以分析更大的问题，并大大减少验证时间相比，国家的最先进的技术，结合经典的POR方法与符号算法和其他实现反例引导抽象细化技术。
2010-03-19 cs.LO cs.SE
Automated Repair of AI Code with Large Language Models and Formal Verification
The University of Manchester（曼彻斯特大学）；Federal University of Amazonas（亚马逊联邦大学）
本研究针对AI代码的内存安全漏洞问题，通过程序变异扩展NeuroCodeBench数据集，结合ESBMC形式化验证工具与大语言模型实现漏洞自动修复，并对比了多种提示工程技术及迭代调用方法的修复性能。
2024-05-14 cs.AI cs.SE
ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification
The University of Manchester（曼彻斯特大学）
提出一种自上而下的组合验证工具ConVer，利用大语言模型合成函数合约，并通过CEGAR-CEGIS循环迭代精炼合约，以解决大规模C程序形式化验证中的状态空间爆炸问题。
2026-05-26 cs.AI cs.SE
Incremental Bounded Model Checking for Embedded Software (extended version)
程序分析在嵌入式系统开发中处于主流的边缘。基于有界模型检验的自动化验证工具在行为需求的形式化验证、发现运行时错误和自动化测试用例生成等方面有着广泛的应用。现有的嵌入式软件的工业工具使用现成的有界模型迭代，并应用它来验证程序与越来越多的解绕。这种方法不必要地浪费时间重复已经完成的工作，并且无法利用增量SAT求解的能力。本文报告了软件模型检查器CBMC的扩展，以支持增量有界模型检验和它的成功集成与工业嵌入式软件验证工具BTC EmbeddedTester。我们提出了一个广泛的评估大型工业嵌入式程序，这表明，增量有界模型检验削减运行时间的一个数量级相比，标准的非增量方法，使应用程序的形式化验证大型和复杂的嵌入式软件。
2014-09-20 cs.SE
Property-Driven Fence Insertion using Reorder Bounded Model Checking
现代体系结构提供的内存一致性保证比顺序一致性要弱。这些较弱的保证允许程序表现出程序语句似乎已经按照程序顺序执行的行为。幸运的是，如果需要，现代体系结构提供了内存屏障（栅栏）来强制执行一对语句之间的程序顺序。由于弱内存模型的复杂语义，即使对于有经验的程序员来说，栅栏的放置也是一个挑战。栅栏太少会导致bug，而过度使用栅栏会导致性能下降。这促使了围栏的自动放置。恢复程序中顺序一致性的工具可能会插入比程序正确所需的更多的栅栏。因此，我们提出了一个属性驱动的技术，引入“重新排序有界的探索”，以确定最小数量的程序位置围栏放置。我们在CBMC之上实现了我们的技术;然而，原则上，我们的技术足够通用，可以用于任何模型检查器。我们的实验结果表明，我们的技术是更快，解决更多的相关基准的实例相比，早期的方法。
2015-06-01 cs.SE
Can Large Language Models Model Programs Formally?
State Key Laboratory for Novel Software Technology, Nanjing University（南京大学）；The Hong Kong University of Science and Technology（香港科技大学）；Guangzhou HKUST Fok Ying Tung Research Institute（广州港科技霍英东研究院）
本文提出Model-Bench，通过将Python程序转换为可验证的模型检查规范，评估和提升大语言模型在程序建模方面的能力，揭示了LLMs在程序建模上的局限性。
2026-04-02 cs.SE
Inferring Loop Invariants by Mutation, Dynamic Analysis, and Static Checking
验证器可以证明程序正确的对他们的全部功能规格要求，为程序与循环，额外的注释形式的循环不变量-属性，保持每次迭代的循环。我们表明，显着的循环不变的候选人可以通过系统地突变后置条件，然后，动态检查（基于自动生成的测试）淘汰无效的候选人，和静态检查选择可证明有效的。我们提出了一个自动应用这些技术来支持程序证明器的框架，为无需手动编写循环不变式的全自动验证铺平了道路：适用于28种方法（包括39个不同的循环）从不同的java.util类（偶尔修改，以避免使用静态检查器不完全支持的Java功能），我们的EQUIPATE原型自动履行了97%的证明义务，这导致了28种方法中的25种的自动完全正确性证明-优于用于全自动验证的几种最先进的工具。
2016-02-05 cs.SE
A Benchmark Suite and Ground-Truth Methodology for Formal Verification of IEC 61131-3 Ladder Diagram Programs
University of Manchester（曼彻斯特大学）；Federal University of Amazonas (UFAM)（亚马孙联邦大学）
针对PLC程序形式化验证缺乏标准基准的问题，提出首个结合受控真值与ST/LD编码覆盖的基准套件，含50程序83变体，通过三方真值纪律和跨工具验证确保可靠性，并发布开放工件。
2026-09-17 cs.AR cs.CL cs.SE
Equivalence, Identity, and Unitarity Checking in Black-Box Testing of Quantum Programs
本文提出三种新算法，解决量子程序黑盒测试中的等价性、同一性和幺正性检查问题，并优化参数选择，实验验证其有效性。
2024-05-24 cs.SE quant-ph
Computation of WCET using Program Slicing and Real-Time Model-Checking
在现代复杂体系结构上计算精确的WCET是一项具有挑战性的任务。在过去的十年里，这个问题已经引起了很多关注，但仍然存在一些悬而未决的问题。首先，需要二进制程序的控制流图（CFG）来计算WCET，并且使用生成二进制代码的编译器的一些内部知识来构建此CFG;此外，一旦构建了CFG，就必须手动注释循环边界。其次，计算WCET的算法（结合了抽象解释和线性规划）是为特定的架构量身定制的：改变架构（例如用ARM9替换ARM 7）需要设计一个新的自组织算法。第三，计算结果（使用可用的工具获得）的紧密性没有与在真实硬件上测量的实际执行时间进行比较。在本文中，我们解决上述问题。我们首先描述了一个全自动的方法来计算一个CFG完全基于二进制程序进行分析。其次，我们将硬件的模型描述为时间自动机的产物，并且该模型独立于程序描述。在硬件上运行的程序的模型是通过将程序（的自动机）与硬件的（时间自动机）模型同步来获得的。计算WCET减少到一个可达性问题的同步模型和解决使用模型检查UPPAAL。最后，我们提出了一个严格的方法，使我们能够比较我们的计算结果，在一个真正的平台，ARM920 T上测量的实际执行时间。
2011-11-08 cs.SE
Automatic Coding Rule Conformance Checking Using Logic Programs
提高程序可靠性的一些方法涉及程序设计语言的有纪律的使用，以便最小化由容易出错的特征引入的危险。这是通过编写代码来实现的，该代码被约束到先验容许程序的子集，并且，此外，可以仅使用语言的子集。这些子集由所谓的编码规则的集合确定。
2007-11-02 cs.PL cs.SE
Model Checking with Program Slicing Based on Variable Dependence Graphs
在嵌入式控制系统中，由于软件复杂性导致例如与时序相关的问题，软件缺陷的潜在风险一直在增加。这些缺陷很少通过测试或模拟发现。为了检测这种缺陷，我们提出了一种建模方法，可以生成软件模型的模型检验与程序切片技术的基础上的变量依赖图。最后将该方法应用于一个汽车控制软件的实例中，验证了该方法的有效性。此外，我们开发了一个软件工具来自动化模型生成，并取得了35%的总验证时间减少模型检验。
2013-01-01 cs.LO 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
Combining Genetic Programming and Model Checking to Generate Environment Assumptions
当环境假设未被考虑时，软件验证可能产生虚假故障。环境假设是系统或组件对其操作环境的预期，通常根据该系统或组件的输入条件进行指定。在这篇文章中，我们提出了一种方法来自动推断网络物理系统（CPS）的环境假设。我们的方法以三种不同的方式改进了最先进的技术：首先，我们学习涉及信号和数值变量的复杂CPS模型的假设;第二，学习的假设包括定义在多个变量上的算术表达式;第三，我们确定了环境假设的可靠性和信息量之间的权衡，并证明了我们的方法在优先考虑这些标准时的灵活性。我们评估我们的方法使用公共领域基准的CPS模型从洛克希德·马丁公司和卫星控制系统的一个组成部分，卫星系统供应商LuxSpace。结果表明，我们的方法优于国家的最先进的技术学习假设的CPS模型，而且，当应用到我们的工业CPS模型，我们的方法是能够学习的假设是足够接近的假设人工开发的工程师是有实用价值的。
2021-01-06 cs.SE
Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version)
本文提出将外部辅助不变量注入基于 Craig 插值的软件模型检查算法，并在 CPAchecker 中实现，减少插值查询、提升效率且解决了现有工具无法处理的验证任务。
2024-10-25 cs.SE
Direct Construction of Program Alignment Automata for Equivalence Checking
检查两个程序在语义上是否等价的问题有着广泛的应用，因此具有非常重要的意义。有几种技术可以解决这个问题，主要是通过构建一个产品程序，使其更容易获得有用的不变量。一个新的除了这些是一种技术，使用对齐谓词来对齐两个程序的痕迹，以构建一个程序对齐自动机。由谓词引导不仅有利于处理句法差异，而且有利于保持与属性的相关性。然而，基于跟踪的技术也存在缺点。获得覆盖所有程序行为的跟踪是困难的，并且任何欠近似都可能导致不完整的产品程序。此外，这种间接结构不知道缺失的行为，并且无法控制上述不完整性。针对这些问题，本文提出了一种直接构造程序对齐自动机的算法。
2021-09-04 cs.FL cs.SE
A shallow dive into the depths of non-termination checking for C programs
针对现有非终止性检查工具在现实程序上效果不佳的问题，提出一种基于有界模型检查的健全高效技术，通过循环内断言与迭代展开深度检查循环状态，实验表明优于现有工具。
2024-09-04 cs.LO cs.SE
BTOR2-Based C Program Verification via Hardware Model Checking
East China Normal University（华东师范大学）
研究如何将C程序验证任务编码为BTOR2模型，提出C2Btor方法，该方法用程序计数器等进行相关表示与映射。通过在基准测试上与其他工具比较，C2Btor解决任务更多，尤其在比特向量基准测试上效果好，让C程序验证受益于硬件模型检查后端进展。
2026-07-21 cs.FL 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
Synthesis of Parametric Programs using Genetic Programming and Model Checking
Bar Ilan University（巴伊兰大学）
形式化方法应用基于数学原理的算法来增强系统的可靠性。尝试从验证、模型检验或根据系统的正式规范测试系统到自动构建系统，这是很自然的。经典的算法综合理论提供了有趣的算法，但也令人震惊的高复杂性和不可判定性的结果。结合模型检验和测试，遗传编程的使用提供了一个强大的启发式综合程序。该方法不是完全自动的，因为它由设置规格和参数的用户进行微调。它也不能保证总是成功并收敛到满足所有所需属性的解决方案。然而，我们成功地将其应用于相当重要的示例，并设法找到解决方案，以应对困难的编程挑战，以及改进和纠正代码。我们在这里描述了几个版本的我们的方法合成顺序和并发系统。
2014-02-27 cs.AI cs.NE cs.SE
Fault Localization in Multi-Threaded C Programs using Bounded Model Checking (extended version)
软件调试是一个非常耗时的过程，对于多线程程序来说，由于线程调度算法的不确定性行为，这一过程甚至更糟。然而，如果使用自动方法来定位故障，则可以大大减少调试时间。在这项研究中，提出了一种新的方法，故障定位，在多线程的C程序。它将多线程程序转换为相应的顺序程序，然后使用适合于这类程序的故障诊断方法，以定位故障。代码转换是用来自反例的规则和上下文切换信息实现的，反例通常由有界模型检查器生成。实验结果表明，该方法是有效的，在这样一种方式，顺序故障定位方法可以扩展到多线程程序。
2015-09-08 cs.LO cs.SE
Contract Based Program Models for Software Model Checking
本文提出在组件状态转换性质已演绎验证的基础上，利用 flow graphs 低成本构建独立于语言的抽象程序模型，并规划支持 C 语言安全关键嵌入式软件验证的工作流与工具链。
2025-03-14 cs.FL cs.SE
Distributed Bounded Model Checking
程序验证是一项耗费大量资源的任务。本文着眼于并行化SMT为基础的自动程序验证，特别是有界模型检查，使其可以分布和执行的机器集群的问题。我们提出了一个算法，动态展开的程序的调用图，并经常分裂它创建子任务，可以并行解决。该算法是自适应的，根据可用资源控制拆分速率，并且还利用来自SMT求解器的信息来拆分搜索中最复杂的地方。我们实现了我们的算法，通过修改CORRAL，微软的静态驱动程序验证器（SDV）使用的验证器，并评估它的一系列硬SDV基准。
2020-05-16 cs.PL cs.SE
Tailoring Stateless Model Checking for Event-Driven Multi-Threaded Programs
针对事件驱动多线程程序，提出Event-DPOR算法，通过扩展Optimal-DPOR并采用高效冗余检查，指数级提升SMC验证效率并避免不必要探索。
2023-07-29 cs.PL cs.SE
Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness
本文提出了一个通用的框架和方法，在一个高层次的分布式算法的完整的编程和检查，在伪代码语言，但精确指定和直接执行，在正式的规约语言和实用的程序设计语言，分别。检查框架，以及分布式算法的编写和它们的安全性和活性属性的规范，使用DistAlgo，一种用于分布式算法的高级语言。我们给出了一个完整的可执行规范的检查框架，一个完整的例子算法和例子的安全性和活性属性。
2020-12-24 cs.DC cs.SE
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
Applying Model Checking to Highly-Configurable Safety Critical Software: The SPS-PPS PLC Program
许多粒子加速器的一个重要方面是不断发展和频繁的配置变化，需要执行它们设计的实验。这通常会导致可配置软件的设计，可以吸收这些变化，并执行所需的控制和保护行动。这种设计策略最大限度地降低了工程和维护成本，但它使软件验证活动更具挑战性，因为必须保证任何可能的配置的安全属性。软件模型检验是一种广泛应用的自动化验证技术。这种验证方法探索系统模型的所有可能组合，以保证其符合某些属性或规范。这对于高度可配置的软件来说是一种非常合适的技术，因为通常有大量的组合需要检查。本文介绍了如何PLCverif，欧洲核子研究中心的模型检验平台，已被应用到一个高度可配置的可编程逻辑控制器（PLC）程序，SPS人员保护系统（PPS）。这种验证方法的好处和挑战也进行了讨论。
2022-03-30 cs.SE cs.SY eess.SY
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
PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C
提出PyVeritas框架，利用LLM将Python转换为C，结合有界模型检验和基于MaxSAT的故障定位，实现Python代码的形式化验证与错误定位，转换准确度达80-90%。
2025-08-11 cs.AI cs.SE
Program Dependence Net and On-demand Slicing for Property Verification of Concurrent System and Software
针对并发软件模型检查中的状态爆炸问题，提出基于Petri网的程序依赖网（PDNet）及其按需切片方法，统一模型避免转换，减少冗余计算，显著降低验证成本。
2023-11-15 cs.FL cs.SE
Model Checking C Programs with Loops via k-Induction and Invariants
我们提出了一种新的证明归纳算法，它结合了k-归纳法和不变量模型检查C程序有界和无界循环。k-归纳算法由三种情况组成：在基本情况下，我们的目标是找到一个反例，最多有k个循环展开;在正向条件下，我们检查循环是否已经完全展开，以及安全属性P是否在k个展开内的所有状态下都成立;在归纳步骤中，我们检查每当P对k个展开成立时，它在系统的下一个展开后也成立。对于k-归纳算法的每一步，我们使用仿射约束来推断不变量（即，多面体）指定前置和后置条件。利用多面体的不变量和不变量两种不同的方法实现了该算法，并对结果进行了比较。实验结果表明，两种形式都能处理多种安全属性，而采用多面体的k-归纳算法解决了更多的验证任务，证明了归纳算法有效性的提高。
2015-02-09 cs.LO cs.SE
Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens
无状态模型检验（SMC）是一种并发程序的验证技术，它通过探索所有可能的线程冲突来检查安全违规。当与动态偏序约简（DPOR）结合时，它是非常有效的，DPOR引入了一个等价类，并且在每个等价类中只需要探索一个。即使使用DPOR，SMC也经常花费不必要的努力来探索纯循环迭代，即，对程序状态没有影响。我们提出的技术，使SMC与DPOR更有效的纯循环迭代程序。第一种是静态程序分析，用于检测循环纯度和相关的程序转换，称为部分循环纯度消除，插入假设语句以阻止纯循环迭代。随后，其中一些假设被转换为await语句，完全删除了许多假设阻止的执行。最后，我们提出了一个扩展的标准DPOR等价，通过削弱事件之间的冲突关系。所有这些技术被纳入一个新的DPOR算法，最佳DPOR等待，它可以处理等待和较弱的冲突关系，是最佳的意义上，它只探索一个执行在每个等价类，也可以诊断活锁。我们在Nidhugg中的实现表明，这些技术可以显着加快并行程序的分析，这些程序目前对SMC工具来说是具有挑战性的，无论是探索其完整的交织集，还是检测其中的并发错误。
2022-08-19 cs.PL cs.SE
Checking the HAL Interface Specification Continuously, Right from the Start
University of Freiburg（弗赖堡大学）；Hahn-Schickard Institute（汉-希克哈德研究所）；Offenburg University（奥芬堡大学）
本文提出了一种持续检查HAL接口规范的方法，从开发一开始就进行检查，通过多次迭代开发嵌入式应用程序，确保每个步骤的检查成功。
2025-12-18 cs.LO cs.SE
Software Model Checking via Summary-Guided Search (Extended Version)
本文提出GPS算法，利用基于摘要的静态分析引导状态搜索，实现软件模型检测，能同时证明安全性和发现错误，并在SV-COMP等基准上优于现有工具。
2025-09-08 cs.PL cs.SE
Bounded Invariant Checking for Stateflow Programs
状态流模型是复杂的软件模型，通常用作Matlab Simulink设计的安全关键软件解决方案的一部分。它们包含了通常很难正式验证的设计原则。特别是，标准的详尽的形式化验证技术不太可能很好地扩展工业中开发的复杂设计。此外，Stateflow语言缺乏形式化的语义，这也阻碍了形式化的分析。为了解决这些挑战，我们奠定了一个可扩展的技术的基础，可证明正确的形式分析的Stateflow模型，相对于不变的属性，有界模型检验（BMC）的基础上符号执行。我们的技术的关键是：i）Stateflow模型的状态空间表示为模型的符号配置上的符号转换系统（STS），作为BMC的基础，以及ii）应用增量BMC，在每次展开转换系统的下一个状态关系后生成验证结果。为此，我们开发了一个符号结构操作语义（SSOS）的状态流，从现有的结构操作语义（SOS），并显示两者之间的不变属性的保存。接下来，我们定义了符号配置上STS的有界不变检验作为一个可满足性问题。我们开发了一个自动生成的初始和下一个状态的STS谓词的过程，并提出了一个编码方案的有界不变的检查问题作为一组约束条件，准备自动分析标准，现成的可满足性求解器。最后，我们提出了初步的性能结果，通过应用我们的工具上一个说明性的例子。
2021-11-19 cs.FL cs.SE
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
Datalog-based Scalable Semantic Diffing of Concurrent Programs
当修改演进程序以解决与线程同步相关的问题时，需要确认改变是正确的，即，它不会引入意外的行为。然而，手动比较两个程序以识别语义差异是劳动密集型的并且容易出错，而基于模型检验的技术在计算上是昂贵的。为了填补这一空白，我们开发了一种快速的近似静态分析来计算两个程序的同步差异。该方法是快速的，因为它不依赖于重量级模型检验技术，而是利用基于多项式时间数据日志的程序分析框架来计算差分数据流边缘，即，一个程序允许的边缘，而另一个程序不允许。虽然使用近似，我们的方法是足够准确的，由于精心设计的数据流推理规则和迭代增加所需的数据流边缘表示的差异。我们已经实现了我们的方法，并在大量的多线程C程序上对其进行了评估，以确认其通常在几秒钟内产生与人类获得的相同差异的能力;相比之下，基于模型检验的现有技术需要几分钟甚至几小时，因此可能会慢10倍到1000倍。
2018-07-16 cs.PL cs.SE
Design-Time Conformance Checking for Pulse-Level Quantum Control
Embry-Riddle Aeronautical University（安柏瑞德航空大学）
针对脉冲级量子控制程序可能超出设备限制的问题，提出设计时检查器qconform，利用版本化能力描述符离线确定程序可实现性，经差分测试验证其可靠性并修复缺陷。
2026-10-08 cs.SE quant-ph
Conditional Model Checking
软件模型检验是一个不可判定的问题，它有三种可能的结果：（1）程序满足规格说明，（2）程序不满足规格说明，（3）模型检验失败。第三种结果通常表现为空格、超时或验证工具的一个组件放弃;在所有这些失败的情况下，验证工具在失败之前执行了大量计算，但没有报告结果。我们建议将模型检查问题重新表述如下，以便即使在失败的情况下，验证工具也能报告所执行工作的摘要：给定一个程序和一个规范，模型检查器返回一个条件P -通常是一个状态谓词-这样程序在条件P下满足规范-也就是说，只要程序不离开满足P的状态。我们当然对返回尽可能弱的条件P的模型检查器感兴趣。代替结果（1），模型检查器将返回P = true;代替（2），条件P将返回满足规范的状态空间部分;在情况（3）中，条件P可以总结模型检查器在空间超时，超时或放弃之前所执行的工作。如果需要完全验证，则可以使用不同的验证方法或工具来关注违反条件的状态。我们给这样的条件作为输入的条件模型检查器，这样的验证问题被限制在状态空间的一部分，满足条件。我们的实验表明，重复应用条件模型检查器，使用不同的条件，可以显着提高验证结果，状态空间覆盖率和性能。
2011-09-30 cs.PL 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
The Output-Space Hypothesis: Enumerative Equivalence Checking for Tensor Programs
University of Pennsylvania（宾夕法尼亚大学）
提出输出空间假设，通过翻转量词检查单个输出位置对所有输入的等价性，实现张量程序更一致的错误发现，在6988个AI编写的CUDA内核中找出600个隐藏错误。
2026-09-18 cs.LG cs.PL cs.SE
LLMs are Brittle to Simple Code Transformations: Introducing CETBench - A Benchmark for Code-Equivalence Checking
Indian Institute of Technology Delhi（印度理工学院德里分校）；IBM Research AI（IBM研究院）
本文提出CETBench基准，通过对程序对施加随机代码变换生成等价性检查数据，发现简单变换即可显著降低SOTA LLMs的性能，并提出基于微调的方法加以改进，揭示LLMs在代码语义理解上仍存在明显不足。
2026-10-21 cs.CL cs.LG cs.PL
Generating Counterexamples for Model Checking by Transformation
反例解释了为什么所需的时间逻辑属性无法保持。反例的产生被认为是模型检验作为一种验证技术的主要优点之一。此外，当模型检验确实成功地验证了属性时，通常不存在可用作已验证属性的证据的独立可检验见证。在此之前，我们已经展示了程序转换技术如何用于验证反应系统的安全性和活性特性。然而，没有反例或证人使用所描述的技术产生。在本文中，我们将讨论这个问题。特别是，我们展示了如何程序转换技术蒸馏可以用来促进反应系统的时间属性的反例和证人的建设。示例系统的目的是相互排斥模型进行分析，使用这些技术的安全性（相互排斥）和活性（非饥饿），与反例生成的那些属性不举行。
2016-07-08 cs.LO 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
EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking
Stanford University（斯坦福大学）；MIT（麻省理工学院）；Google（谷歌）；Nanjing University（南京大学）；Intel（英特尔）
本文提出 EquiBench 基准，通过等价性检查评估大语言模型对程序语义的推理能力，发现现有模型在困难类别上仅略优于随机基线，且多依赖语法相似性而非真正的语义推理。
2025-09-19 cs.AI cs.CL cs.LG
DAG-width of Control Flow Graphs with Applications to Model Checking
由结构化程序产生的控制流图的树宽最多为6。然而，由于控制流图本质上是有向的，因此考虑有向图的宽度度量是有意义的。我们使用所谓的DAG宽度，并表明，DAG宽度的控制流图所产生的结构化（goto自由）的程序是最多三个。此外，我们还给出了一个线性时间算法来计算这些控制流图的DAG分解。这个结果的一个结果是，奇偶游戏（因此$μ$ -演算模型检验问题），这是已知的有界DAG宽度的图上是易处理的，可以有效地解决在控制流图的实践。
2015-03-03 cs.DM cs.LO cs.PL
