Abstraction Logic: The Marriage of Contextual Refinement and Separation Logic
上下文细化和分离逻辑是本质上非常不同的成功的验证技术。首先，前者保证了具体程序和抽象程序之间的行为细化，而后者保证了具体程序在一定条件下的安全性（用前置条件和后置条件表示）。第二，前者不允许任何假设的背景下，局部推理的模块，而后者允许丰富的假设。在本文中，我们提出了一种新的验证技术，称为抽象逻辑（AL），固有地结合上下文细化和分离逻辑，如虹膜和VST，从而采取两者的优势。具体来说，AL允许我们在分离逻辑风格的外部模块的前置和后置条件下，针对抽象模块本地验证具体模块。AL在Coq中完全形式化，并提供了一种证明模式，该模式支持使用我们自己的策略的模拟式推理和使用IPM（虹膜证明模式）的SL式推理的组合。使用证明模式，我们验证了各种例子，以证明推理的所有权（基于部分交换幺半群）和纯度（$i.e.$，终止没有系统调用），循环和高阶推理的相互递归和函数指针，可重用和逐步验证通过中间抽象。此外，验证结果与CompCert相结合，使我们正式建立从顶级抽象程序的行为细化，一直到他们的汇编代码。
2021-09-07 cs.PL
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction
数组操作程序的自动验证是一个具有挑战性的问题，因为它往往相当于归纳量化循环不变量的推理，在某些情况下，甚至可能不是一阶可表达的。在本文中，我们提出了一种新的验证技术，这是基于归纳的用户定义的排名程序状态作为一种替代循环不变。我们的技术，被称为归纳降秩，分为两步。首先，我们简化了验证问题，证明了当输入状态包含长度为B或更小的输入数组时，程序是正确的，使用数组的长度作为状态的秩。其次，我们利用一个压缩函数g将一个长度> B的数组的程序状态sigma转换为一个长度小于等于1的数组的状态g（sigma），证明了当g满足一定的自然条件时，如果程序违反了sigma的规范，那么它也违反了g（sigma）的规范。程序对任意长度数组的输入的正确性由归纳法得出。我们使我们的技术自动数组程序的执行长度是成比例的输入数组的长度，（i）执行的第一步使用符号执行，（ii）验证所需的条件g使用Z3，和（iii）提供一个启发式的过程合成g。我们实现了我们的技术，并成功地将其应用到几个有趣的arraymanipulating程序，包括双向求和程序，其循环不变量不能表示在一阶逻辑，而其规范是量词自由。
2021-06-02 cs.CC cs.PL
Invariant Synthesis for Incomplete Verification Engines
Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）；Amazon India（亚马逊印度）；University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）
我们提出了一个框架，综合归纳不变量不完整的验证引擎，健全的逻辑问题，在不可判定的理论，可判定的理论。我们的框架是基于反例引导归纳合成原理（CEGIS），并允许验证引擎沟通非证明性信息，以指导不变的合成。我们精确地展示了验证引擎如何计算这种非可证明性信息，以及如何构建有效的学习算法时，不变量表示为一组固定的谓词的布尔组合。此外，我们评估我们的框架中的两个验证设置，一个是验证引擎需要处理量化的公式，一个是验证引擎必须对堆属性的原因表示在一个富有表现力的，但不可判定的分离逻辑。我们的实验表明，我们的不变量合成框架的基础上的不可证明性信息，可以有效地合成归纳不变量，并充分加强合同在一个大的程序套件。
2018-01-12 cs.LG cs.LO cs.PL
Ownership Types for Verification of Programs with Pointer Arithmetic
本文扩展Toman等人结合所有权与精化类型的低级程序验证类型系统以支持指针算术，证明可靠性并实现原型工具，实验表明可自动验证无断言错误。
2023-12-11 cs.PL
VyZX: Formal Verification of a Graphical Quantum Language
University of Chicago（芝加哥大学）；University of St Andrews（圣安德鲁斯大学）
本文提出VyZX库，用于验证归纳定义的图式语言，通过证明ZX-calculus重写规则的正确性，结合证明助手技术实现图式语言的正式推理。
2026-04-08 cs.PL quant-ph
A Fresh Look at Best Inductive Loop Invariant Synthesis for Bit-Vector Relations
The State Key Laboratory of Blockchain and Data Security, Zhejiang University（浙江大学区块链与数据安全国家重点实验室）
针对程序分析中最佳归纳不变式综合的效率挑战，提出基于一阶理论量化约束优化的新公式及两种位向量程序算法，在基准测试中性能优于传统方法，可解决更多基准并提升高位宽下的扩展性与验证效果。
2026-07-30 cs.PL
Finding Inductive Loop Invariants using Large Language Models
Microsoft Research（微软研究院）；Cornell（康奈尔大学）；IIT Kanpur（印度理工学院坎普尔分校）
本文利用大型语言模型生成归纳循环不变量，并通过符号工具验证其正确性，实验表明该方法能提升自动化程序验证的性能。
2023-11-14 cs.LG cs.PL
Synchronous Programming with Refinement Types
本文提出 CPS 语言 MARVeLus 的形式化，构建其同步细化类型系统元理论，实现验证与实现在同一语言中的结合，并在真实系统上验证同步程序执行。
2024-09-04 cs.PL
A Relational Logic for Higher-Order Programs
关系程序验证是程序验证的一种变体，其中可以推理两个程序，并且作为一种特殊情况，可以在不同的输入上对单个程序进行两次执行。关系程序验证可用于推理广泛的属性，包括等价性和精化，以及诸如连续性、信息流安全性或相对成本等专门概念。在高阶环境中，关系程序验证可以使用关系精化类型系统来实现，关系精化类型系统是断言具有关系解释的一种精化类型。关系精化类型的系统擅长于将结构上等价的项关联起来，但是对于将结构非常不同的项关联起来，提供的支持有限。本文提出了一种逻辑，称为关系高阶逻辑（RHOL），用于证明具有归纳类型和递归定义的简单类型$λ$ -演算的关系性质。RHOL保留了关系精化类型系统的类型导向风格，但通过同时推理两个术语的规则以及只考虑两个术语之一的规则实现了更大的表达性。我们表明，RHOL具有强大的基础，通过证明与高阶逻辑（HOL）的等价性，并利用这种等价性来推导关键的元理论属性：主题约简，可接受的传递性规则和集合理论的合理性。此外，我们定义了几个现有的关系类型系统，如关系细化类型和依赖分析和相对成本的类型系统的声音嵌入，我们验证的例子是以前的工作无法达到的。
2017-03-15 cs.PL
Extensible Datasort Refinements
细化类型将类型检查转变为轻量级验证。精化类型的经典形式是归并精化，其中归并标识归纳数据集的子类。现有的类型系统要求在声明一个类型时指定该类型的所有细分;同一类型的多个细分只能通过复制类型定义来获得，从而复制代码。我们丰富了传统的签名的概念，它描述了居民的港口，允许重新完善通过签名扩展，而不重复的定义。由于任意更新的签名可以无效的反演原则用于检查情况下的表达式，我们开发了一个定义的签名格式良好，确保扩展保持现有的反演原则。这个定义允许程序的不同部分以不同的方式扩展相同的签名，而不会相互冲突。每个部分都可以独立地进行类型检查，允许单独编译。
2020-11-14 cs.PL
Programming Language Features for Refinement
数学和数据细化是研究得很好的主题，它们提供了一种数学上严格的方法，可以逐步引入软件实现中的细节。程序细化是在某些程序设计语言的上下文中执行的，但是主流语言缺乏在程序文本中记录细化步骤序列的功能。为了试验精化、自动验证和语言设计的组合，已将精化特性添加到验证感知的程序设计语言Dafny中。本文介绍了这些功能，并反映了一些初步的使用。
2016-06-07 cs.PL cs.SE
Refinement Types for TypeScript
我们提出了Refined TypeScript（RSC），这是一个轻量级的TypeScript细化类型系统，可以对高阶命令式程序进行静态验证。我们开发了一个正式的RSC核心，描绘了细化类型和可变性之间的相互作用。接下来，我们扩展核心来解释TypeScript的命令式和动态特性。最后，我们在一组真实世界的基准测试中评估了RSC，包括Octane基准测试、D3、Transducers和TypeScript编译器的一部分。
2016-04-08 cs.PL
Refinement types in Jolie
Jolie是微服务的第一种语言，目前它是动态类型检查的。本文认为有机会集成动态和静态类型检查与细化类型的介绍，通过SMT求解器验证。这两个方面的集成允许内部服务的静态验证和（潜在恶意的）外部服务的动态验证合作的场景，以减少测试工作并增强安全性。
2016-02-22 cs.PL cs.SE
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules (Technical Report)
提出一种基于CompCert内存模型和带内存保护的Kripke关系的开放模块可信组合编译方法，实现直接精化，支持完整编译链的端到端验证，降低验证复杂度。
2023-11-18 cs.PL
Refinement Reflection: Complete Verification with SMT
我们介绍了精化反射，一个新的框架，用于建立基于SMT的演绎验证。关键思想是将实现用户定义函数的代码反映到函数的（输出）细化类型中。因此，在使用函数时，函数定义以允许可判定验证的精确方式在SMT逻辑中实例化。反射允许用户通过使用模式匹配和递归来编写其他程序来编写程序的等式证明，以执行大小写分解和归纳。因此，通过命题作为类型的原则，我们表明，反射允许规范的任意功能的正确性属性。最后，我们介绍了一个证明搜索算法，称为证明逻辑评估，使用技术从模型检验和抽象的解释，完全自动化的等式推理。我们已经在Liquid Haskell中实现了反射，并使用它来验证Monoid，Applicationative，Functor和Monad类型类的广泛使用的实例实际上满足使客户端安全所需的关键代数定律，并使用反射构建了第一个库，该库实际验证了关于关联性和排序的假设，这些假设对于安全的确定性并行性至关重要。
2017-11-09 cs.LO cs.PL
Automating and Mechanizing Cutoff-based Verification of Distributed Protocols
分布式协议通常是参数化的，并且可以在具有任意数量节点的系统上执行，因此证明其正确性成为无限状态验证问题。验证分布式协议最常用的方法是找到一个足够强的归纳不变量来证明所需的安全性。然而，发现归纳不变量是众所周知的困难，尤其是在分布式协议的背景下，这是非常复杂的，由于其异步性质。在这项工作中，我们研究了一种基于正交截止的方法来验证分布式协议，该方法避开了寻找归纳不变量的问题，而是将检查正确性降低到有限状态验证问题。其主要思想是找到一个有限的、固定的协议实例，称为截断实例，如果截断实例是安全的，那么任何协议实例也是安全的。以前的截止为基础的方法只适用于一类有限的协议和规范。我们形式化的截断方法的通用协议建模语言（RML）的上下文中，并确定充分的条件，可以有效地编码在SMT检查是否一个给定的协议实例是一个截止实例。此外，我们提出了一个简单的静态分析为基础的算法，自动合成一个截止的实例。我们已经成功地应用我们的方法在一些复杂的分布式协议，提供了第一个已知的截止结果，其中许多。
2022-11-28 cs.DC cs.PL
Type-directed Bounding of Collections in Reactive Programs
我们的目标是静态验证，在一个给定的反应式程序中，集合变量的长度不会超过一个给定的界限。我们提出了一个可扩展的基于类型的技术，检查每个集合变量有一个给定的细化类型，指定其长度的约束。我们的细化类型的一个新特性是，细化可以引用AST计数器，这些计数器跟踪AST节点执行了多少次。此功能使类型细化能够跟踪有限的流敏感信息。我们生成验证条件，以确保AST计数器的使用一致，并且类型暗示给定的界限。验证条件由现成的SMT求解器排出。实验结果表明，我们的技术是可扩展的，有效地验证反应式程序的集合长度的要求。
2019-01-28 cs.PL
Mechanizing Refinement Types (extended)
基于精化类型的实用检查器使用隐式语义子类型和参数多态性的组合来简化规范并自动验证程序的复杂属性。然而，一个正式的元理论会计的完善型系统使用这种组合已被证明是难以捉摸的。我们提出了一个结合语义子类型和参数多态性的核心精化演算λ_RF。我们开发了这个演算的元理论，并证明了类型系统的可靠性。最后，我们使用基于精化类型的LiquidHaskell作为证明检查器，给出了我们的元理论的完整机械化，展示了精化如何用于机械化。
2022-07-12 cs.PL
Flux: Liquid Types for Rust
我们介绍Flux，它展示了逻辑改进如何与Rust的所有权机制一起工作，以产生符合人体工程学的基于类型的低级指针操作程序的验证。首先，我们为Rust设计了一个新的精炼类型系统，该系统索引可变位置，纯（不可变）值可以出现在精炼中，然后利用Rust的所有权机制来抽象Rust多态类型构造函数中位置的子结构推理，同时支持强更新。我们通过利用堆叠借用别名模型来形式化对Rust的强别名保证的关键依赖，以证明“良好类型程序的良好借用评估不会卡住”。其次，我们在Flux中实现了我们的类型系统，Flux是Rust编译器的一个插件，它利用复杂不变量到类型和细化的因素来有效地合成循环注释-包括描述容器内容的复杂量化不变量-通过液体推理。第三，我们评估通量与基准套件的向量操作程序和部分先前验证的安全沙箱库，以证明在最先进的Prusti验证器中实现的程序逻辑的优势，细化类型。虽然Prusti更具表现力的程序逻辑通常可以验证深层功能正确性规范，但对于我们的基准测试所涵盖的轻量级但普遍存在的重要验证用例，液体类型使验证符合人体工程学，将规范行削减了两倍，验证时间减少了一个数量级，注释开销从代码大小的24%（平均9%）减少到根本没有。
2022-11-14 cs.PL
Inductive Program Synthesis over Noisy Datasets using Abstraction Refinement Based Optimization
Massachusetts Institute of Technology（麻省理工学院）
我们提出了一种新的综合算法来解决噪声数据集上的程序合成，即，可能包含不正确/损坏的输入输出示例的数据。我们的算法使用了一个抽象的细化为基础的优化过程来合成程序，优化的噪声数据集的损失和合成程序的复杂性之间的权衡。该算法使用抽象来划分程序的搜索空间为子空间，通过计算一个抽象值，表示在一个子空间中的所有程序的输出。抽象值允许我们的算法计算，为每个子空间，一个声音的近似下界的损失在所有的程序在子空间。它迭代地细化这些抽象，以进一步将空间细分为更小的子空间，修剪不包含最优程序的子空间，并最终合成最优程序。我们在一个叫做Rose的工具中实现了这个算法。我们使用SyGuS 2018基准套件将Rose与当前最先进的嘈杂程序合成系统进行比较。我们的评估表明，Rose的性能明显优于之前的系统：在从SyGus 2018基准测试套件中提取的两个有噪声的基准测试程序合成问题集上，Rose提供了高达1587和81.7的加速比，中值加速比为20.5和81.7。Rose还终止了20个（共54个）和4个（共11个）比以前的系统多的基准问题。罗斯和以前的系统合成的程序是最佳的噪声数据集。对于基准测试集中的大多数问题（$286$中的$272$），合成程序还为原始（未见过的）无噪声数据集中的所有输入产生正确的输出。这些结果突出了玫瑰可以提供有效的嘈杂程序合成的好处。
2021-04-27 cs.FL cs.LG cs.PL
Conditional Contextual Refinement (CCR)
上下文精化（CR）是指定开放程序的标准概念之一。CR有两个主要优点：（i）（水平和垂直）组合性，其允许我们将大的上下文细化分解成许多较小的细化，从而实现模块化和增量验证，以及（ii）对编程特征没有限制，从而允许，例如，相互递归、指针值传递和高阶函数。然而，CR有一个缺点，它不能对上下文施加条件，因为它量化了所有上下文，这确实在支持完整的组合性和编程特性方面发挥了关键作用。在本文中，我们解决的问题，找到一个概念的细化，满足所有三个要求：支持完整的组合性，完整的（顺序）编程功能，并在上下文丰富的条件。作为一种解决方案，我们提出了一种新的细化理论，称为CCR（条件上下文细化），并开发了一个验证框架的基础上，它允许我们模块化和增量验证一个具体的模块对一个抽象的模块分离逻辑风格的前和后条件下的外部模块。它在Coq中完全形式化，并提供了一种证明模式，该模式结合了（i）关于保留IO事件和终止等副作用的模拟推理和（ii）关于前置和后置条件的命题推理。此外，验证结果与CompCert相结合，使我们正式建立从顶级抽象程序的行为细化，一直到他们的汇编代码。
2022-03-14 cs.LO cs.PL
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine
我们正式验证一个抽象的机器调用的值的alcuda演算与de Bruijn条款，简单的替代，和小步语义。我们遵循逐步改进的方法，从一个带有替换的朴素堆栈机器开始。然后，我们细化到一个具有闭包的机器，最后是一个具有为闭包提供结构共享的堆的机器。我们证明了三个细化步骤的正确性与组成小步自下而上的模拟。有一个附带的Coq开发验证所有结果。
2019-01-02 cs.LO cs.PL
Verifying C11-Style Weak Memory Libraries via Refinement
演绎验证的并发程序在弱内存下，到目前为止，仅限于简单的程序在一个单一的状态空间。对于可伸缩性，我们还需要具有可验证库抽象的模块化技术。本文解决了这一挑战的背景下，RC 11 RAR，C11内存模型的一个子集，允许放松和释放获取访问，但不允许，所谓的，负载缓冲周期。我们开发了一个简单的框架，用于指定抽象对象，精确地描述了抽象方法调用的可观察性保证。我们展示了如何将这个框架与一个操作语义集成在一起，该操作语义可以验证客户端程序从他们使用的库中执行抽象方法调用。最后，我们将展示如何实现这样的抽象在RC 11 RAR可以验证通过开发一个（上下文）细化框架的抽象对象。我们的框架，包括操作语义，客户端库程序的验证技术，和抽象库和它们的实现之间的模拟，已在伊莎贝尔/HOL机械化。
2021-08-16 cs.LO cs.PL
Decidability and Synthesis of Abstract Inductive Invariants
在许多软件和硬件验证系统中，在给定域范围内的归纳不变量的可判定性和综合起着重要的作用。我们认为在这里归纳不变量属于一个抽象域$A$的定义在抽象的解释，即，确保存在的最佳逼近$A$的任何系统属性。在这种情况下，我们研究的可判定性存在的抽象归纳不变量的$A$的过渡系统和相应的算法合成。我们的模型依赖于一些一般性的结果，这些结果将抽象归纳不变量的存在性与过渡系统的传递函数的$A$中的最佳正确逼近的最小不动点及其完备性联系起来。这种方法使我们能够推导出可判定性和合成结果的抽象归纳不变量，适用于著名的基尔达尔的常数传播和卡尔的仿射等式抽象域。此外，我们表明，最近的一般算法合成归纳不变量域的逻辑公式，可以系统地从我们的结果和推广到一系列的算法计算抽象归纳不变量。
2020-04-09 cs.LO cs.PL
Towards establishing formal verification and inductive code synthesis in the PLC domain
如今，形式化方法被用于各种领域，用于程序的验证或用于从模型生成代码生成，以提高软件的质量并降低成本。然而，仍然有一些领域，其中正式的方法没有被广泛采用，尽管提供了大量的可能的好处。这是可编程逻辑控制器（PLC）领域的情况。本文的目的是评估PLC开发的背景下，形式化方法的潜力。为此，形式化方法的一般概念，首先介绍，然后转移到PLC领域，从而在工程为导向的描述的技术是基于PLC开发的共同概念。基于此描述，我们采访了具有不同经验的PLC专业人员，以了解他们对该主题的看法，并确定PLC领域中可能的用例。调查结果表明，该技术在PLC领域具有很高的潜力，无论是作为直接支持开发人员的工具，还是作为基于模型的系统工程工具链中的关键元素。调查结果的评估是在演示应用程序的帮助下进行的，该应用程序与西门子的全集成自动化门户进行通信，并通过基于模型的开源代码生成器Fastsynth生成程序。基于行业相关PLC项目的基准测试显示出令人满意的合成时间，并成功集成到PLC开发人员的工作流程中。
2021-06-30 cs.FL cs.PL cs.SE
Aiming Low Is Harder -- Induction for Lower Bounds in Probabilistic Program Verification
我们提出了一个新的归纳规则，用于验证概率循环执行后的随机变量的期望值的下界以及它们的预期运行时间。我们的规则是简单的，因为循环体语义只需要经常应用，以验证候选确实是下界。特别是，它不需要像许多以前的规则那样找到序列的极限。
2021-08-11 cs.LO cs.PL
A Practical Approach to Interval Refinement for math.h/cmath Functions
C++程序的验证已经在几个领域取得了相当大的进展，但对于使用这些语言的数学库的程序来说却没有。原因是，所有广泛使用的库都不能保证计算结果。这似乎阻止了对使用它们的程序进行形式化验证的任何尝试：没有函数的规范，就不能静态地得出关于程序行为的结论。我们提出一个投降的替代方案。我们引入了一种实用的方法，利用大多数math.h/cmath函数几乎是分段单调的这一事实：正如我们通过详尽测试发现的那样，它们可能会出现小故障，通常大小非常小，数量也很少。我们开发的间隔细化技术，这些功能的基础上修改的二分法搜索，使验证通过符号执行基于模型检验，抽象的解释，和测试数据生成。我们的细化算法是文献中第一个能够处理非正确舍入函数实现的算法，能够在最常见的实现中进行验证。我们实验评估我们的方法在现实世界的代码，显示其检测或排除异常行为的能力。
2020-08-11 cs.LO cs.PL cs.SE
Structural Temporal Logic for Mechanized Program Verification
本文提出结构化时序逻辑 Ticl，将复杂（共）归纳证明编码为结构化引理，支持在证明助手中以高抽象层次对调度、并发共享内存和分布式共识程序进行安全性与活性性质的组合式机械化验证。
2025-08-21 cs.LO cs.PL
Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement
LMU Munich（慕尼黑大学）
本文提出了一种基于并行轨迹抽象细化的多线程软件模型检查方法，通过利用多核CPU提升验证效率，优于传统顺序方法和DSS技术。
2026-01-15 cs.LO cs.PL cs.SE
Model Sketching by Abstraction Refinement for Lifted Model Checking (Extended Version)
在这项工作中，我们展示了如何使用验证和分析技术的模型家庭（软件产品线）的数字功能提供了一个有趣的技术，合成完整的模型从草图（即\具有孔的部分模型）。特别是，我们提出了一种方法，用于合成Promela模型草图使用特定于变量的抽象细化解除（基于家庭）模型检验。
2021-12-21 cs.LO cs.PL
Higher-Order Constrained Horn Clauses and Refinement Types
出于高阶函数程序自动验证中的应用，我们开发了一个概念的约束霍恩条款在高阶逻辑和决策问题，其可满足性。我们表明，虽然高阶子句的可满足系统一般不具有最小模型，有一个规范模型的概念，通过减少到一种单调逻辑程序的问题。在高阶程序验证的工作之后，我们开发了一个细化类型的系统，以推理和自动搜索模型。这为解决决策问题提供了一个合理但不完整的方法。最后，我们证明了一个扩展的决策问题，其中细化类型直接用作警卫存在量词可以减少到原来的问题。这个结果可以用来表明，高阶函数的性质，可定义使用细化类型也表示使用高阶约束霍恩子句。
2017-08-01 cs.LO cs.PL
Domain-Type-Guided Refinement Selection Based on Sliced Path Prefixes
摘要抽象是软件验证中的一种成功技术，而在不可行错误路径上的插值是在反例引导的抽象精化中自动检测正确抽象级别的一种成功方法。由于插值有一个显着的影响，抽象的质量，因此，验证的有效性，一个算法，用于获得最佳的可能的插值是可取的。我们提出了一种分析无关的技术，使得它可以从一个给定的不可行的错误路径，如果有几个原因不可行的错误Path.We输入给定的不可行的错误路径，并应用切片技术，以获得一组错误路径，比原来的错误路径更抽象，但仍然是不可行的，每一个不同的原因。新路径的（更抽象的）约束可以被传递到标准插值引擎，以便获得一组插值序列，每个新路径一个。然后分析可以从这组插值序列中选择并选择最合适的，而不是被绑定到插值引擎通常返回的单个插值序列。例如，我们可以根据插值中变量的域类型进行选择，更喜欢避免循环计数器，或者与潜在循环不变量的模板进行比较，从而控制在程序抽象中出现的信息类型。我们在开源验证框架CPAchecker中实现了新算法，并表明我们的证明技术无关的方法显著提高了验证过程的有效性和效率。
2015-01-31 cs.PL cs.SE
Solving Horn Clauses on Inductive Data Types Without Induction
基于归纳定义的数据结构，如列表和树，我们解决了约束Horn子句（CHC）的可满足性验证问题。我们提出了一种转换技术，其目标是删除这些数据结构的CHCs，从而减少其满足性的整数和布尔CHCs的可满足性问题。我们提出了一个转换算法，并确定了一类条款，它总是成功的。我们还考虑了该算法的扩展，它结合了子句转换与整数约束推理。通过实验评估，我们表明，我们的技术大大提高了Z3求解器的有效性，CHCs。我们还表明，我们的验证技术的基础上CHC转换，然后CHC解决方案，是有竞争力的CHC求解器与归纳扩展。本文件正在考虑被TPLP接受。
2018-04-24 cs.LO cs.PL
Ranking LLM-Generated Loop Invariants for Program Verification
Microsoft Research（微软研究院）
针对LLM生成循环不变式需多次采样导致验证器调用过多的问题，提出一种对比排序器对候选不变式重新排序，显著提升了正确不变式的排名并减少了验证器调用次数。
2024-02-12 cs.AI cs.CL cs.PL
HELMHOLTZ: A Verifier for Tezos Smart Contracts Based on Refinement Types
DaiLambda, Inc.（DaiLambda公司）；Kyoto University（京都大学）
智能合约是在区块链上执行的程序，许多加密货币都是在此基础上实现的，并被用于自动化交易。由于智能合约涉及大量资金，因此对一种可以静态和正式验证它们的方法的需求激增。本文介绍了我们为Michelson开发的基于类型的静态验证工具HELMHOLTZ，这是一种基于静态类型的堆栈语言，用于编写在区块链平台Tezos上执行的智能合约。HELMHOLTZ是在我们对迈克尔逊类型系统的细化类型扩展之上设计的。HELMHOLTZ以用户定义的规范（以精化类型的形式编写）注释迈克尔逊程序作为输入;然后根据精化类型系统的规范对程序进行类型化，使用SMT求解器Z3释放生成的验证条件。我们简要地介绍了我们的精化类型系统的核心演算迈克尔逊的迷你迈克尔逊，它结合了特征，如复合数据集（例如，列表和对）、高阶函数和调用另一个合约。\HELMHOLTZ{}成功地验证了几个实用的迈克尔逊程序，包括一个向帐户转账和检查数字签名的程序。
2021-09-10 cs.CL cs.LO cs.PL
