A shallow dive into the depths of non-termination checking for C programs
针对现有非终止性检查工具在现实程序上效果不佳的问题，提出一种基于有界模型检查的健全高效技术，通过循环内断言与迭代展开深度检查循环状态，实验表明优于现有工具。
2024-09-04 cs.LO 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
Fault Localization in Multi-Threaded C Programs using Bounded Model Checking (extended version)
软件调试是一个非常耗时的过程，对于多线程程序来说，由于线程调度算法的不确定性行为，这一过程甚至更糟。然而，如果使用自动方法来定位故障，则可以大大减少调试时间。在这项研究中，提出了一种新的方法，故障定位，在多线程的C程序。它将多线程程序转换为相应的顺序程序，然后使用适合于这类程序的故障诊断方法，以定位故障。代码转换是用来自反例的规则和上下文切换信息实现的，反例通常由有界模型检查器生成。实验结果表明，该方法是有效的，在这样一种方式，顺序故障定位方法可以扩展到多线程程序。
2015-09-08 cs.LO cs.SE
Slicing Concurrent Constraint Programs
并发约束编程（CCP）是一个声明式的并发模型，其中代理通过告诉和询问共享存储中的约束（信息片段）进行交互。以前的一些作品已经开发了（近似）CCP语言的声明式调试器。然而，调试并发程序的任务仍然很困难。在本文中，我们定义了一个动态切片CCP，我们表明它是一个有用的伴侣工具，现有的调试技术。我们的技术首先考虑一个部分计算（跟踪），显示存在的错误。通常，这种跟踪中的信息量是压倒性的，用户很容易迷失方向，因为她不能专注于bug的来源。我们的切片器允许标记计算状态的一部分，并帮助用户消除大部分冗余信息，以突出错误。我们表明，这种技术可以定制CCP的定时变量。我们还开发了一个原型实现免费提供实验。
2017-02-10 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
Scaling Bounded Model Checking By Transforming Programs With Arrays
有界模型检验是发现程序缺陷最成功的技术之一。然而，模型检查器是资源饥渴，往往无法验证程序循环迭代在大型arrays.We提出了一个转换，使有界模型检查器验证某一类数组属性。我们的技术将数组操作（ANSI-C）程序转换为无数组和无循环（ANSI-C）程序，从而显着降低了模型检查器的资源需求。转换后的程序的模型检验使用现成的有界模型检验器有效地模拟循环迭代。因此，我们的转换程序是一个健全的抽象的原始程序，也是精确的，在大量的情况下-我们正式的类的程序，它保证是精确的。我们在行业规范和学术基准上证明了我们的技术的适用性和有用性。
2017-03-07 cs.LO
Dynamic Backward Slicing of Rewriting Logic Computations
跟踪切片是一种广泛使用的执行跟踪分析技术，可有效地用于程序调试、分析和理解。在本文中，我们提出了一个反向跟踪切片技术，可用于重写逻辑理论的分析。我们的跟踪切片技术使我们能够系统地追溯重写序列模方程公理（如结合性和交换性）的算法，动态简化的痕迹，通过检测控制和数据的依赖关系，并丢弃无用的数据，不影响最终结果。我们的方法是特别适合于分析复杂的，文本大系统的计算，如那些交付的反例的痕迹，由莫德模型检查。
2011-06-06 cs.LO
Dynamic Consistency Checking in Goal-Directed Answer Set Programming
在回答集编程中，当程序上的约束变得不可满足时，就会出现不一致。在本文中，我们介绍了一种技术，为我们的目标导向的方法计算答案集的动态一致性检查，只有那些被认为是相关的部分答案集的约束进行测试，允许不一致的知识库被成功地查询。然而，该算法保证，如果一个程序至少有一个一致的答案集，返回的任何部分答案集将是某个一致答案集的子集。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2014-05-14 cs.LO
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
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
Model Checking as Program Verification by Abstract Interpretation (Extended Version)
本文提出将模型检验视为程序验证，引入MOKA语言把时序逻辑公式编码为程序，并结合抽象解释与局部完全抽象动态精化分析精度，从而复用更一般的抽象并避免误报。
2025-06-05 cs.LO
Epistemic Model Checking for Knowledge-Based Program Implementation: an Application to Anonymous Broadcast
知识为基础的程序提供了一个抽象的协议，其中代理人的行动是有关他们的知识状态的描述。本文介绍了如何认识模型检验技术可能会被应用到发现和验证具体的实现基于这个抽象层次的描述。实现的细节取决于协议使用的特定上下文。基于知识的方法使得实现能够相对于这些使用条件进行优化。该方法说明使用扩展的用餐密码协议，匿名广播的安全协议。
2010-04-26 cs.DC cs.LO
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
Stateless Model Checking for POWER
我们提出了第一个框架，有效地应用无状态模型检验（SMC）的程序下运行的放松内存模型的权力。该框架结合了几项贡献。第一个贡献是，我们开发了一个计划，系统地从现有的公理化的操作执行模型。该计划是这样的，派生的执行模型非常适合高效的SMC。我们将我们的计划的一个公理模型的权力。我们的主要贡献是一种技术，高效SMC，称为松弛无状态模型检验（RSMC），系统地探讨了可能的不等价执行的程序。RSMC是适合使用我们的计划获得的执行模型。我们证明了RSMC是健全的，最佳的POWER内存模型，在这个意义上，每个完整的程序行为探索一次。我们显示我们的技术的可行性，通过提供一个实现C/pthreads编写的程序。
2016-05-07 cs.LO
Scaling Bounded Model Checking By Transforming Programs With Arrays
有界模型检验是发现程序缺陷最成功的技术之一。然而，对于在大型数组上进行循环迭代的程序，有界模型检查器通常会超出其可用资源的限制。我们提出了一个转换，使有界模型检查器，以验证某一类数组属性。我们的技术将ANSI-C中的数组操作程序转换为无数组和无循环的程序。转换后的程序可以有效地验证一个现成的有界模型检查。虽然变换后的程序是，在一般情况下，原程序的抽象，我们正式表征的性质，变换是精确的。我们在行业规范和学术基准上证明了我们的技术的适用性和有用性。
2016-08-17 cs.LO cs.PL
Auto-Tuning High-Performance Programs Using Model Checking in Promela
本文提出利用模型检查中的反例加速高性能程序自动调优，以OpenCL程序为例，结合Promela和SPIN工具实现并验证了该方法。
2023-05-16 cs.DC cs.LO
CurryCheck: Checking Properties of Curry Programs
我们提出CurryCheck，一个工具来自动测试的功能逻辑程序设计语言咖喱写的程序。CurryCheck执行单元测试以及通过一个或多个参数进行参数化的属性测试。在后一种情况下，CurryCheck通过系统地枚举测试用例来测试这些属性，以便对于较小的有限域，CurryCheck可以实际证明属性。可以在Curry模块中定义单元测试和属性，而无需导出。因此，它们对于记录源代码的预期语义也很有用。此外，CurryCheck还支持自动检查源程序中出现的规范和合同。因此，CurryCheck是一个有用的工具，有助于基于属性和规范的可靠和测试良好的声明性程序的开发。
2016-08-19 cs.LO cs.PL
Model Checking Temporal Properties of Recursive Probabilistic Programs
本文研究了递归概率程序（pPDA）针对 $ω$-可见下推语言的模型检测问题，给出了可判定性与复杂性结果，证明 CaRet 等逻辑可指定过程调用与返回匹配等结构化性质。
2023-12-14 cs.FL cs.LO
SMT-based Model Checking for Recursive Programs
提出了一种基于SMT的递归程序安全性验证的符号模型检验算法。该算法是模块化的，并单独分析程序。与其他基于SMT的方法不同，它既保持了程序摘要的“过度近似”，也保持了程序摘要的“欠近似”。欠近似用于分析过程调用，而无需内联。过近似用于阻止不可行的反例和检测收敛到一个证明。我们表明，程序和属性的可判定理论，该算法是保证找到一个反例，如果存在的。然而，效率依赖于用于量词消去（QE）的预言。对于布尔程序，该算法是一个多项式决策过程，匹配最佳BDD算法的最坏情况的界限。对于线性算术（整数和有理数），我们通过“懒惰地”应用QE给出了算法的有效实例。我们使用现有的插值技术来过度近似QE，并引入“基于模型的投影”来欠近似QE。在SV-COMP基准测试上的实验结果表明，该算法在最新水平上有了显著的改进。
2014-05-25 cs.LO
Bounded Model Checking of Pointer Programs Revisited
指针程序的有界模型检验是一种调试技术，用于操作堆上动态分配的指针结构的程序。它基于以下四点意见。第一，错误条件（如悬空指针的解引用）可以用双变量一阶逻辑的~片段来表示。其次，片段在最弱的前提条件wrt下是封闭的。有限路径第三，数据结构，如树、列表等，可以通过在数据库片段中定义的归纳谓词来表达。最后，双变量逻辑和数据库的两个片段的组合是可判定的。在本文中，我们通过扩展底层逻辑的表达能力来改进这种技术。在~序列的例子中，我们证明了新的逻辑是能够建模更复杂的数据结构与更复杂的依赖堆和更复杂的分析。
2016-02-29 cs.LO cs.PL
Abstraction and Acceleration in SMT-based Model-Checking for Array Programs
抽象（以其各种形式）是模型检验中一种强大的既定技术;然而，当涉及无界数据结构时，它并不总是以令人满意的方式处理发散现象。加速是一种广泛应用的避免发散的方法，但它主要应用于整数规划。本文讨论了无界数组的加速转换关系问题，最终目标是避免抽象程序可达性分析过程中的发散。为此，我们首先设计了一种格式来计算在这个域中的加速度，然后我们展示了如何适应所谓的“单调抽象”技术，以有效地处理复杂的公式与嵌套的量词所产生的加速预处理。值得注意的是，我们的技术可以很容易地插入到抽象/细化循环，并大大有助于避免发散：与MCMT模型检查器进行的实验证明了我们的方法对具有无界数组的程序的有效性，如果单独应用加速和抽象/细化技术，则会失败。
2013-10-03 cs.LO
An Overview of the HFL Model Checking Project
在这篇文章中，我们给出了一个概述我们的项目高阶程序验证的基础上HFL（高阶不动点逻辑）模型检验。在简要介绍HFL之后，我们解释了如何将其应用于程序验证，并总结了该项目的现状。
2021-09-10 cs.LO cs.PL
SMT-based Symbolic Model-Checking for Operator Precedence Languages
针对现有POTL显式状态模型检测方法可扩展性差的问题，本文提出首个基于SMT的符号化方法，将POTL公式与程序模型编码为SMT公式，通过求解器以有界模型检测方式搜索反例轨迹，实验验证了方案有效性。
2024-05-18 cs.LO
A Type Checking Algorithm for Higher-rank, Impredicative and Second-order Types
我们研究了一种类型检查算法，它能够对使用高阶、非谓词和二阶类型等功能的函数式程序的非平凡子类进行类型检查。算法唯一需要类型注释的地方是在每个函数声明之前。我们证明了系统$\mathbf{F}_ω$的类型检查算法的可靠性，即如果程序是类型检查，那么类型检查器将产生一个良好类型的注释系统$\mathbf{F}_ω$术语。我们扩展了基本算法来处理模式匹配和let绑定。我们实现了一个原型类型检查器，并测试了各种功能的程序。
2017-11-13 cs.LO cs.PL
Eliminating Unfounded Set Checking for HEX-Programs
Technische Universität Wien（维也纳工业大学）
HEX程序是应答集编程（ASP）范例的扩展，其通过所谓的外部原子将外部计算手段并入声明性程序设计语言中。它们的语义是根据Faber-Leone-Pfeifer（FLP）约简的最小模型定义的。开发本地解算器的HEX程序的基础上适当的概念，无根据的集合一直受到最近的研究效率的原因。虽然这导致了使用FLP约简的朴素最小性检查的改进，但对发现性的测试仍然是一项计算昂贵的任务。在这项工作中，我们提高了在这方面的HEX程序评估确定的语法类的程序，可以有效地识别，并允许完全跳过的foundedness检查。此外，我们开发的标准分解成组件的程序，这样的搜索无根据集可以受到限制。观察到我们的结果适用于许多HEX程序的应用程序提供了分析证据，我们的方法的意义和有效性，这是补充了初步的实验验证的简要讨论。
2013-01-08 cs.AI cs.LO
Combining Static and Dynamic Contract Checking for Curry
静态类型系统通常不足以表达对函数调用的所有要求。因此，带有前置和后置条件的契约可以用来表达对操作的更复杂的约束。可以在运行时间检查协定，以确保仅使用合理的参数调用操作并返回预期的结果。虽然这种动态契约检查提供了更可靠的程序执行，但它需要执行时间，并可能导致程序崩溃，这些崩溃可能会在编译时用更高级的方法检测到。为了改善这种情况的声明性语言，我们提出了一种方法，结合静态和动态的合同检查的功能逻辑语言咖喱。基于函数式逻辑程序设计中契约检验的形式化模型，提出了一种在编译时自动检验契约的方法。如果合同验证成功，则可以省略对合同的动态检查。这种方法减少了执行时间，而不会降低可靠的程序执行。在最好的情况下，当所有契约都被静态验证时，它提供了对软件的信任，因为在程序执行期间不会发生由于违反契约而导致的崩溃。
2017-09-14 cs.LO cs.PL
PEQcheck: Localized and Context-aware Checking of Functional Equivalence (Technical Report)
重构不得改变程序的功能。然而，并不是所有的重构都满足这个要求。因此，必须明确检查重构不会改变功能。由于很少有一个正式的规格说明程序的行为，我们利用原来的程序作为功能规范。然后，我们检查原始程序和重构后的程序在功能上是否等价。为此，我们采用一个共同的想法，减少等价性检查程序验证。为了提高效率，我们的等价性检查PEQcheck构造一个验证任务，每个重构的代码段，而不是一个功能，通常由以前的工作。此外，PEQcheck考虑代码段的上下文。例如，只有被修改的和活的变量才需要是等效的，只读变量可以在原始代码段和重构的代码段之间共享。此外，我们的评估证明，本地化和上下文感知检查执行的\peqcheck确实可以是有益的。
2021-03-22 cs.LO cs.PL
Automatic Verification of Timed Concurrent Constraint Programs
时间并发约束（Timed Concurrent Constraint，tccp）是并发约束编程（Concurrent Constraint Programming，cc）范式的扩展，它允许我们指定时间至关重要的并发系统，例如反应式系统。可以有无限多个状态的系统可以在tccp中指定。模型检验是一种能够自动验证具有大量状态的有限状态系统的技术。在过去的几年里，一些研究已经调查了如何扩展模型检验技术的系统具有无限数量的状态。在本文中，我们提出了一种方法，利用tccp的计算模型。基于约束的计算允许我们定义一种方法，将模型检验算法应用于（一类）无限状态系统。我们扩展的经典算法的模型检验LTL的一个特定的逻辑定义的验证tccp和tccp结构，我们在这项工作中定义的建模程序的行为。我们定义了一个限制的时间，以得到一个有限的模型，然后我们开发了一些说明性的例子。据我们所知，这是第一个为tccp定义模型检验方法的方法。
2005-05-11 cs.LO
Functional Equivalence Checking for Verification of Algebraic Transformations on Array-Intensive Source Code
高能效和高性能嵌入式软件的开发越来越依赖于对源代码关键部分进行复杂转换。设计师应用这种非平凡的源代码转换往往面临的问题，以确保功能等效的原始和转换后的程序。目前，他们不得不依赖于不完整和耗时的模拟。形式化的自动验证的转换程序对原来的是可取的。这就需要类似于比较数字电路的等价性检查工具。我们提出了这样一个工具来比较数组密集型相关的程序，通过组合的重要的全球性的转换，如表达式传播，循环和代数变换。当转换后的程序未能通过等价性检查时，该工具会提供有关错误可能位置的具体反馈。
2007-10-25 cs.LO
Checking Termination of Bottom-Up Evaluation of Logic Programs with Function Symbols
近年来，人们越来越关注自自底向上的【形】的复杂术语逻辑程序的语义评估。程序中函数符号的存在可能使基础实例化无限，并且在一般情况下，不再保证模型的有限性和评估过程的终止。由于程序终止问题在一般情况下是不可判定的，最近提出了几个可判定准则（称为程序终止准则）。然而，目前的条件是不能识别甚至简单的程序，其自自底向上的【形】的执行总是终止。本文通过对程序结构的深入分析，提出了一种新的自自底向上的【形】求值下带函数符号的逻辑程序可终止性判定准则。首先，我们分析了复杂的条款之间的传播参数的扩展版本的参数图称为传播图。由此产生的标准，称为伽马-非周期性，概括了迄今为止提出的大多数可判定的标准。接下来，我们研究规则如何相互激活，并定义一个更强大的标准，称为安全性。该标准使用所谓的安全函数，能够分析规则如何相互激活以及规则中某些参数的存在如何限制其激活。我们还研究了所提出的标准绑定查询的应用程序，并表明，安全标准是非常适合识别相关类的程序和绑定查询。最后，我们提出了一个层次的类终止程序，称为k-安全，其中k-安全类严格包括（k-1）-安全类。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2014-07-11 cs.LO
Bounded LTL Model Checking with Stable Models
本文介绍了异步并发系统的有界模型检验，作为回答集编程的一个很有前途的应用领域。作为异步系统的通信自动机，1-安全Petri网的推广模型，使用。它示出了如何1-安全的Petri网和对网络的行为的要求可以被翻译成一个逻辑程序，这样的有界模型检验问题的网可以通过计算相应的程序的稳定模型来解决。稳定模型语义的使用导致有界可达性和死锁检测任务的紧凑编码，以及线性时序逻辑的有界模型检验的更一般的问题。给出了所设计的翻译的正确性证明，并给出了使用该翻译和Smodels系统的一些实验结果。
2003-05-23 cs.AI cs.LO
Bounded Model Checking for Asynchronous Hyperproperties
对机密性的许多类型的攻击源于计算机程序在其中操作的环境的不确定性（例如，同步器和异步通信信道）。在本文中，我们专注于验证的机密性在不确定性环境中的异步超属性的推理。首先，我们概括的时间逻辑A-HLTL允许嵌套的轨迹量化，其中的轨迹确定不同的执行轨迹可能会推进和口吃。我们提出了一个有界的模型检验算法A-HLTL的基础上QBF解决的一个片段的广义A-HLTL和评估并发程序，调度攻击，编译器优化，投机执行，和缓存定时攻击的各种案例研究。我们还严格分析了A-HLTL不同片段的模型检验的复杂性。
2023-01-26 cs.LO
On Model-Checking Higher-Order Effectful Programs (Long Version)
本文从一般视角研究高阶代数效应程序的模型检验，将其视为高阶递归方案，并证明效应处理器在一般情况下导致不可判定性，而在简单语法形式下保持可判定，同时提出通用规范语言的构想。
2023-08-31 cs.LO cs.PL
A Spin-based model checking for the simple concurrent program on a preemptive RTOS
我们通过eChronos将现有的RTOS内核抢占式调度模型从机器辅助证明修改为基于Spin的模型检查器。我们构建的模型可以自动验证，而不是用手工证明。此外，我们还研究了一个类似Linux的实时内核--Piko/RT的设计和ARMv7-M体系结构的规范来重建模型，并在内核开发阶段使用LTL来描述一个简单的并发程序--消费者/生产者问题。我们证明了在抢占式调度和ARMv7-M机制下，程序不会出现竞争条件、饥饿和死锁。
2018-08-07 cs.FL cs.LO cs.OS
Explaining Counterexamples with Giant-Step Assertion Checking
在程序的演绎验证过程中，识别证明失败的原因是困难的：它可能是由于程序中的不正确，程序注释中的不完整性，或者证明器的不完整性。解决证明失败所需的更改取决于其类别，但证明器无法提供任何分类帮助。当使用SMT求解器来履行证明义务时，该求解器可以从失败的尝试中提出一个模型，从中可以导出一个可能的反例。但反例可能是无效的，在这种情况下，它可能会增加更多的混乱而不是帮助。为了检查反例的有效性和分类证明失败，我们提出了两种不同的语义下的运行时断言检查（RAC）执行之间的比较，使用反例作为一个预言。第一次RAC执行遵循正常的程序语义，违反程序注释表示程序中存在错误。第二个RAC执行遵循一个新的“giant-step”语义，它既不执行循环，也不执行函数调用，而是从oracle中检索返回值和修改变量的值。只有在巨步执行下才能观察到的程序注释的违反表征了程序注释的不完整性。我们实现了这种方法在Why 3平台的演绎程序验证和评估它使用的例子从以前的文献。
2021-08-06 cs.LO cs.PL
Foundations for Entailment Checking in Quantitative Separation Logic (extended version)
定量分离逻辑（QSL）是分离逻辑（SL）的扩展，用于概率指针程序的验证。在QSL中，公式计算为实数而不是真值，例如，在给定的符号堆中，内存安全终止的概率。与\SL一样，使用QSL进行推理时的一个关键问题是\emph{entailment}：公式f是否包含另一个公式g？我们给出了从QSL中的蕴涵检查到SL中的蕴涵检查的一般性约简。这允许利用大量的SL研究来自动验证概率指针程序。我们分析了我们的方法的复杂性，并证明其适用性。特别是，我们得到的第一个可判定性结果，验证这些程序通过应用我们的减少到一个量化的扩展著名的符号堆片段的分离逻辑。
2022-01-27 cs.LO cs.PL
Epistemic Model Checking of Atomic Commitment Protocols with Byzantine Failures
Halpern和Fagin提出的基于知识的程序的概念为设计、分析和优化分布式系统提供了一种有用的形式主义。本文将两阶段提交协议描述为一个基于知识的程序，然后通过模型检验和反例引导精化的迭代过程，找到了在拜占庭故障背景下具有同步可靠通信的完美召回语义的程序的具体实现。我们模拟了几种不同类型的拜占庭故障，并验证了不同的策略来对抗和减轻它们。我们解决了一些在以前的文献中没有考虑过的问题，即，在什么情况下发送者可以知道它的传输已经成功，以及在什么情况下代理可以知道协调者正在欺骗，并且找到这些问题的具体答案。本文还介绍了一种基于时间-认知模型检验技术的方法，该方法可以用来验证分布式协议的最短和最长执行时间以及导致它们的场景。
2017-05-10 cs.DC cs.LO
Comparing State-Representations for DEL Model Checking
ILLC, University of Amsterdam（阿姆斯特丹大学计算逻辑与系统研究所）；Chennai Mathematical Institute（金奈数学研究所）
本文比较了 DEL 模型检查中符号结构和心理程序的表示方法，证明了其理论复杂性，并提供了两种转换的直接方法。
2025-11-27 cs.LO cs.MA
Deciding Asynchronous Hyperproperties for Recursive Programs
本文提出一种带新机制识别迹位置的异步超性质逻辑，在保持有限状态模型检测复杂度不变且更具表达力的同时，首次为递归程序超性质模型检测提供了合适方法。
2023-10-25 cs.FL cs.LO cs.PL
Proving Safety with Trace Automata and Bounded Model Checking
循环欠近似是一种技术，它通过额外的分支来丰富C程序，这些分支代表了（有限的）循环迭代范围的效果。虽然这种技术可以显著地加速错误的检测，但它引入了冗余的执行跟踪，这可能使程序的验证复杂化。这对于基于有界模型检验的验证工具尤其如此，该工具结合了简化的算法来确定是否已经考虑了循环的所有可行迭代。我们提出了一种技术，使用\emph{trace automata}，以消除执行循环加速后的冗余执行。该方法减小了分析下的程序的直径，这在某些情况下足以允许使用有界模型检验的安全性证明。我们的转换是精确的-它不会引入假阳性，也不会掩盖任何错误。我们已经实现了分析作为一个源到源的转换，并提出了实验结果显示该技术的适用性。
2014-10-21 cs.FL cs.LO cs.PL
Checking Robustness Between Weak Transactional Consistency Models
对数据库的并发访问通常封装在事务中，以便能够与其他并发计算隔离并对故障具有弹性。现代数据库为事务提供了各种语义，对应于一致性和可用性之间的不同权衡。由于较弱的一致性模型提供更好的性能，因此一个重要的问题是调查给定程序所需的最弱一致性级别（以满足其规范）。作为处理这个问题的一种方式，我们调查的问题，检查是否一个给定的程序具有相同的一组行为时，更换一个较弱的一致性模型。这种被称为鲁棒性的特性通常意味着在削弱一致性时保留程序的任何规范。我们专注于一致性模型的鲁棒性问题，这是弱于标准的串行化，即因果一致性，前缀一致性，快照隔离。我们发现，检查这些模型之间的鲁棒性是多项式时间减少到一个状态可达性问题下的串行化。我们使用这种减少也得到一个务实的证明技术的基础上，利普顿的减少理论，允许证明程序的鲁棒性。我们已经将我们的技术应用于几个具有挑战性的应用程序，从分布式系统和数据库的文献。
2021-01-22 cs.LO cs.PL
Refinement Type Directed Search for Meta-Interpretive-Learning of Higher-Order Logic Programs
University of Oxford（牛津大学）；St. John’s College（圣约翰学院）
在归纳逻辑程序设计（ILP）社区中的程序合成问题通常被视为无类型的。我们考虑了用户提供的类型对背景知识的好处。在元解释学习（MIL）框架的基础上，我们证明了类型检查能够修剪程序的大部分假设空间。引入多态类型检查的MIL方法逻辑程序合成验证强有力的理论和实验结果，显示了立方减少的搜索空间和合成时间的大小，在类型化的背景谓词的数量。此外，我们能够推断多态类型的合成条款和整个程序。另一个进步是开发了一种在ILP中利用精化类型的方法。在这里，我们表明，进一步修剪的搜索空间可以实现，虽然SMT解决用于细化类型检查来
2021-02-18 cs.AI cs.LO
Strong Equivalence for LPMLN Programs
Arizona State University（亚利桑那州立大学）
LPMLN是一个概率扩展的答案集程序的权重方案改编自马尔可夫逻辑。我们研究了LPMLN中强等价的概念，这是一个有用的数学工具，简化了LPMLN程序的一部分，而不看它的其余部分。我们表明，在LPMLN中的强等价性的验证可以减少到等价性检查，在经典逻辑通过约简和选择规则，以及在“软”逻辑下的等价性检查这里和那里。结果使我们能够利用答案集求解器进行LPMLN强等价性检查。该研究还建议我们使用选择规则，这里和那里的逻辑和经典逻辑的LPMLN语义的一些重新表述。
2019-09-18 cs.AI cs.LO
Model checking Branching-Time Properties of Multi-Pushdown Systems is Hard
我们解决了多下推系统的共享内存并发程序的模型检验问题。我们认为在这里布尔程序与有限数量的线程和递归过程。众所周知，这类程序的模型检验问题是不可判定的。在本文中，我们调查的可判定性和这个问题的复杂性的假设下，有界的上下文切换定义的Qadeer和Zeroof，和相位有界的La Torre等人提出的。对时间逻辑，特别是分支时间逻辑，如模态$μ$ -演算或CTL的模型检验这样的系统很少受到关注。众所周知，与模态$μ$ -演算密切相关的奇偶博弈对于有界相位系统类是可判定的（因此对于有界上下文切换也是如此），但具有非初等复杂性（赛斯）。一个自然的问题是，这种高复杂性是否是不可避免的，有什么方法来绕过它。本文解决这些问题，不幸的是，有点令人惊讶的是，它表明，分支模型检验的MPDS本质上是一个很难的问题，没有简单的解决方案。我们证明了在相位限制下的MPDS上的奇偶博弈是非初等的。我们的主要结果表明，模型检验的$k$上下文有界MPDS对一个简单的CTL片段，由公式，其时间运营商来自集合${\EF, \EX}$，有一个非初等的下界。
2012-05-31 cs.FL cs.GT cs.LO
