IC3 Modulo Theories via Implicit Predicate Abstraction
我们提出了一种新的方法来推广的IC3算法不变检查从有限状态到无限状态的过渡系统，表示在一些背景理论。该过程是基于IC3与隐式（谓词）抽象的紧密集成，隐式（谓词）抽象是一种表示抽象转换而不显式计算抽象系统的技术，并且相对于谓词的增加是增量的。在这种情况下，IC3只在抽象状态空间的布尔级别上操作，发现抽象谓词上的归纳子句。理论推理被限制在底层SMT求解器中，并在执行可满足性检查时透明地应用。当当前的抽象允许一个虚假的反例时，它通过发现和添加足够的新谓词集来改进。重要的是，这可以以完全增量的方式完成，而不会丢弃在前一次搜索中找到的子句。所提出的方法有两个关键优点。首先，与IC 3当前的SMT泛化不同，它允许处理广泛的背景理论，而不依赖于临时扩展，例如量词消去或特定于理论的从句泛化程序，这些程序可能并不总是可用的，而且可能效率低下。其次，与直接探索具体的转换系统相比，使用抽象可以显著提高性能，正如我们的实验所证明的那样。
2013-10-25 cs.LO cs.SE
Predicate Abstraction via Symbolic Decision Procedures
我们提出了一种新的方法进行谓词抽象的基础上的符号决策过程。直觉上，一个理论的符号决策过程需要理论中的一组谓词，并在谓词集合上的所有子集上符号地执行决策过程。符号决策过程的结果是一个共享表达式（由有向无环图表示），它隐式地表示谓词抽象查询的答案。我们提出了象征性的决定程序的逻辑等式和未解释的功能（EUF）和差异逻辑（DIFF），并表明这些程序运行在伪多项式（而不是指数）的时间。然后，我们提供了一种方法来构造简单的混合理论（包括上述两个理论）的符号决策程序使用扩展的纳尔逊-奥本组合方法。我们提出了初步评估我们的程序谓词抽象基准从设备驱动程序验证SLAM。
2007-04-24 cs.LO cs.PL cs.SC
Enhancing Predicate Pairing with Abstraction for Relational Verification
关系验证是一种旨在证明两个不同程序片段或两个不同程序运行相关属性的技术。它已被证明，受约束的霍恩子句（CHC）可以有效地用于关系验证，通过应用CHC转换，称为谓词配对，它允许CHC求解器推断不同谓词的参数之间的关系。在本文中，我们研究了如何通过使用基于线性算术的各种抽象域（即，凸多面体的域和它的一些子域）。在提出了一个算法与抽象谓词配对，我们报告的实验，我们已经进行了一百多个关系验证问题，通过使用各种抽象域。实验已经进行了使用VeriMAP转换和验证系统，连同帕尔马多面体库（PPL）和Z3求解器的CHCs。
2017-09-14 cs.LO cs.SE
Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
我们提出了一种方法来约束霍恩子句（CHC）验证相结合的三种技术：抽象的解释在一个域的凸多面体，专门化的约束条件在CHC使用抽象解释的查询答案转换的条款，和细化分裂谓词。的工作的目的是调查如何分析和转换工具开发的约束逻辑程序（CLP）可以适用于霍恩子句验证问题。凸多面体的抽象解释能够推导出复杂的不变量，当与传播约束的专业化结合使用时，它可以经常解决具有挑战性的验证问题。这本身就是一个贡献，但是当它失败时需要精化，并且如何精化凸多面体分析的问题还没有被研究很多。我们提出了一种改进技术的基础上插值来自一个反例跟踪，这些都是用来驱动基于属性的专业化，分裂谓词，进而导致更精确的凸多面体分析。专业化，分析和分裂的过程可以重复，以类似于CEGAR和迭代专业化方法的方式。
2014-12-03 cs.LO
Abstraction Logic: A New Foundation for (Computer) Mathematics
抽象逻辑是一种新的逻辑，是数学的基础。它结合了谓词逻辑和高阶逻辑的特征：抽象逻辑既可以被看作是高阶逻辑减去静态类型，也可以被看作是谓词逻辑加上运算符和变量绑定。我们认为，抽象逻辑是最好的基础逻辑可能，因为它最大限度地提高了简单性和实际的表达能力。这一论点得到了以下观察的支持：抽象逻辑比所有其他一般逻辑具有更简单的术语和更简单的证明概念。同时，抽象逻辑可以形式化直觉主义的和经典的抽象逻辑，并且对于这些逻辑和所有其他用等式扩展演绎逻辑的逻辑都是可靠和完备的。
2022-07-12 cs.LO
Probabilistic Abstractions with Arbitrary Domains
Hermanns等人和Kattenbelt等人最近的工作已经将反例引导的抽象细化（CEGAR）扩展到概率程序。这些方法仅限于谓词抽象。我们提出了一种新的技术，基于Gulavani等人最近引入的抽象可达树，可以使用任意抽象域和加宽运算符（在抽象解释的意义上）。我们展示了如何合适的扩大运营商可以推导出循环不变量难以找到谓词抽象，并提出改进技术。
2011-06-16 cs.LO cs.PL
Abstract Predicate Entailment over Points-To Heaplets is Syntax Recognition
抽象谓词被认为是本文的抽象技术堆分离的配置，并作为真正的Prolog谓词直接翻译成相应的形式语言语法作为验证计划的中间堆状态。所提出的方法是基于规则的，因为抽象谓词是基于规则的，解析技术可以被解释为相应堆图的自动折叠/展开。
2019-06-01 cs.FL cs.LO cs.SC
Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
Seoul National University（首尔大学）
我们在循环不变推理的上下文中解决谓词生成问题。受基于插值的抽象精化技术的启发，我们应用插值定理来合成程序文本隐含的谓词。我们的技术能够提高[14]中基于学习的循环不变推理算法的有效性和效率。我们报告的实验结果的例子，从Linux，SPEC2000，和焦油实用程序。
2012-09-28 cs.LG cs.LO
Generating theorem proving procedures from axioms of Truncated Predicate Calculus
提出了一种新的自动定理证明方法。多项式成本程序，承认属于一个理论的句子生成的基础上的一组公理的所谓的截断谓词演算是一个子集的标准谓词演算。几个示例性的问题，包括显示所提出的方法的性能。
2019-07-29 cs.LO
Modular Abstractions of Reactive Nodes using Disjunctive Invariants
我们希望将反应式程序设计语言（如Lustre）中的节点抽象为具有更简单控制结构的节点，并限制控制状态的数量。为了做到这一点，我们在谓词抽象中计算析取不变量，其中有有限数量的析取，然后我们抽象节点，每个析取代表一个抽象状态。析取不变量的计算是通过使用SMT求解表示的量词消去的形式来执行的。同样的方法也可以用来获得析取循环不变量。
2011-09-09 cs.LO cs.PL
A simple abstraction of arrays and maps by program translation
我们提出了一种处理数组的程序的静态分析方法，数组程序的语义和纯标量操作的语义之间有伽罗瓦连接。实现它的最简单的方法是通过自动地将数组程序语法转换为标量程序，然后使用任何静态分析技术（抽象解释、加速、谓词抽象等）分析标量程序。.).由此获得的标量不变量被翻译回原始程序作为普遍量化的数组不变量。我们说明了我们的方法上的各种例子，导致“荷兰旗”算法。
2015-06-12 cs.LO cs.PL
Dimensional Confluence Algebra of Information Space Modulo Quotient Abstraction Relations in Automated Problem Solving Paradigm
在具有不可数节点的迭代闭多级商图结构中，通过对抽象并行范畴系统的汇流进行拓扑抽象，定义了拓扑度量中的多维变换运算，建立了抽象并行范畴系统中的汇流，实现了网类重写.我们获得的最低先决条件，全面的连接器对多维重写封闭生成汇流在不同的水平和垂直水平的投影模抽象关系构成形式语义的信息空间中的汇流的代数。以形式自动机语法整体表示自动化问题求解范式的分解代数在每个基本抽象关系集、水平结构映射和垂直过程迭代基数下生成丰富多样的多汇流协调器。
2016-12-12 cs.LO
Stochastically timed predicate-based communication primitives for autonomic computing
基于谓词的通信允许系统的组件以多播方式向在执行时通过谓词的评估确定的组件的集合发送消息和请求。基于谓词的通信可以大大简化自治和自适应系统的编程。我们提出了之前工作中引入的软件组件集成语言（SCEL）的随机定时扩展。这样的扩展提出了许多重要的设计和形式语义问题，在不同的抽象层次上有不同的解决方案。我们将讨论其中的四个选项，其中两个更详细。我们提供了一个正式的语义定义和使用的语言建模的自行车共享系统的说明，以及一些初步的系统性能分析。
2014-06-09 cs.LO cs.PL cs.SE
Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification
本文提出一个基于等式谓词、上下文重写和变体化简的归纳推理系统，20条规则中仅9条需用户交互，其余11条可自动执行，大部分已在Maude的NuITP中实现。
2024-05-03 cs.LO
Collapsing Threads Safely with Soft Invariants
规范抽象是一种静态分析技术，它将状态表示为3值逻辑结构，并产生有限的抽象系统。尽管提供了一个有限的边界，这些抽象可能仍然遭受状态爆炸问题。值得注意的是，对于具有任意交错的并发程序，如果状态中的线程基于其位置被抽象，则位置的数量将是状态空间大小的组合因子。我们提出了一种方法，使用规范的抽象，避免这种状态爆炸的“崩溃”的所有线程在一个状态到一个单一的抽象代表。通过定义条件“软不变”插装谓词，保留了将被抽象丢失但验证所需的线程属性。这种技术是用来适应以前的模型验证非阻塞并发数据结构算法的线性化，从而导致指数较小的状态空间。
2015-12-31 cs.LO
Semi-Automated Design Space Exploration for Formal Modelling
基于精化的形式化方法允许通过抽象的增量步骤对系统进行建模。发现正确的抽象层次，制定正确和有意义的不变量，分析错误的模型是使用这种技术时面临的一些挑战。在这里，我们提出了设计空间探索，旨在帮助设计师自动提供高层次的实时建模指导的方法。更具体地说，通过结合常见模式的建模技术，从自动理论形成和自动推理，不同的设计方案进行了探讨，并提出了适当的模型，处理故障。
2016-03-02 cs.LO cs.SE
symQV: Automated Symbolic Verification of Quantum Programs
我们提出了symQV，一个符号执行框架，用于在量子线路模型中编写和验证量子计算。symQV可以自动验证量子程序是否符合一阶规范。我们正式介绍了一个符号量子程序模型。这允许在SMT公式中编码验证问题，然后可以使用delta-完全决策过程进行检查。我们还提出了一个抽象技术，以加快验证过程。实验结果表明，该抽象将symQV的可扩展性提高了一个数量级，可以扩展到具有24个量子比特（2^24维状态空间）的量子程序。
2022-12-05 cs.LO quant-ph
Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms
我们介绍了一种用于容错分布式算法（FTDA）的自动参数化验证方法。FTDA由进程数和假定的拜占庭故障进程的最大数目参数化。在我们的技术的中心是一个参数区间抽象（PIA）的区间边界是参数的算术表达式。使用PIA的数据抽象和一种新形式的计数器抽象，我们减少了参数化的问题，有限状态模型检验。我们证明了我们的方法的实际可行性，通过验证Srikanth和Toueg著名的分布式算法的几个变种。我们的半决策程序的补充和动机的不可判定性证明FTDA验证，即使在没有进程间通信。据我们所知，这是第一篇实现拜占庭FTDA参数化自动验证的论文。
2013-02-03 cs.DC cs.LO
