Automatic Verification of LLVM Code
Axel Legay, Dirk Nowotka, Danny Bøgsted Poulsen
在这项工作中，我们提出了我们的工作，在开发一个软件验证工具的llvm-code - Lodin -它结合了显式状态模型检验，统计模型检验和符号状态模型检验算法。
In this work we present our work in developing a software verification tool for llvm-code - Lodin - that incorporates both explicit-state model checking, statistical model checking and symbolic state model checking algorithms.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Using Off-the-Shelf Exception Support Components in C++ Verification
在软件开发中采用形式化方法的重要一步是支持主流程序设计语言。不幸的是，这些语言通常相当复杂，并且带有大量的标准库。然而，通过选择合适的中间语言，大部分复杂性可以委托给现有的面向执行（而不是面向验证）的编译器前端和标准库实现。在本文中，我们描述了如何支持C++异常可以利用相同的原则。我们的工作是基于DiVM，LLVM派生的，验证友好的中间语言。我们的实现包括两个部分：一个是libunwind平台API的实现，它链接到被测程序，由9个C函数组成。另一部分是LLVM位代码的预处理器，它准备与异常相关的元数据并替换相关的专用LLVM指令。
CANAL: A Cache Timing Analysis Framework via LLVM Transformation
一个统一的建模框架的非功能特性的程序是必不可少的软件分析和验证的研究，因为它减少了负担，个人研究人员实施新的方法和比较现有的方法。我们提出了CANAL，一个框架，通过转换其中间表示LLVM编译器中的程序的缓存行为建模。CANAL在这些变量上插入辅助变量和指令，以允许标准验证工具处理一类新的高速缓存相关属性，例如，用于计算最坏情况下的执行时间和检测侧通道泄漏。我们使用三种验证工具：KLEE，SMACK和Crab-llvm证明了CANAL的有效性。我们确认我们的缓存模型的准确性，通过比较与CPU周期准确的模拟结果GEM 5。CANAL可以在GitHub和YouTube上找到。
Enhancing Translation Validation of Compiler Transformations with Large Language Models
本研究提出融合大语言模型的编译器转换翻译验证框架，以Alive2为基础工具，借助微调LLM预判转换可靠性并结合模糊测试找反例，解决传统形式化工具在LLVM转换等复杂场景的验证局限。
An LLVM Instrumentation Plug-in for Score-P
减少应用程序运行时间，将并行应用程序扩展到更多数量的进程/线程，以及将应用程序移植到新的硬件架构是软件开发过程中的必要任务。因此，开发人员必须调查和理解应用程序运行时的行为。在应用程序执行期间捕获性能相关数据的监控基础设施等工具有助于完成此任务。测量的数据构成了识别瓶颈和优化代码的基础。监控基础设施需要记录应用程序活动的机制，以便进行测量。在大多数应用程序场景中，源代码的自动插装是首选方法。我们为LLVM基础设施引入了一个插件，它可以在编译时实现自动源代码插装。与LLVM/Clang中可用的插装机制相比，我们的插件可以选择性地包含/排除各个应用程序函数。这使开发人员能够将度量微调到所需的细节级别，同时避免由于过多的插装而导致的大量运行时开销。
Inferring Parametric Energy Consumption Functions at Different Software Levels: ISA vs. LLVM IR
程序执行所消耗的能量的静态估计是一个重要的挑战，其在程序优化和验证中具有应用，并且有助于能量感知软件开发。我们的目标是估计这样的能量消耗的形式函数的输入数据大小的程序。我们已经开发了一个工具，用于实验与静态分析推断这样的能量功能在两个级别，指令集架构（ISA）和中间代码（LLVM IR）的水平，并反映它向上到更高的源代码级别。这需要开发从LLVM IR到中间表示的转换及其与现有组件的集成，从ISA到相同表示的转换，资源分析器，ISA级能量模型，以及从该模型到LLVM IR的映射。该方法已应用于在XCore架构上运行的XC语言编写的程序，但足够通用，可以应用于其他语言。实验结果表明，我们的LLVM IR级分析是相当准确的（与硬件测量相比，平均误差小于6.4%），比ISA级分析更强大。本文提供了深入了解在这些级别的精度与可分析性的权衡。
HELIX: Verified compilation of cyber-physical control systems to LLVM IR
HELIX通过代数变换将高性能量算转换为LLVM IR，结合形式化验证确保代码正确性，展示从数学描述到高效实现的全过程。
Instead of Rewriting Foreign Code for Machine Learning, Automatically Synthesize Fast Gradients
将可微分编程技术和机器学习算法应用于外来程序需要开发人员在机器学习框架中重写他们的代码，或者以其他方式提供外来代码的衍生物。本文介绍了酶，一个高性能的自动微分（AD）编译器插件的LLVM编译器框架能够合成梯度的静态分析程序表示的LLVM中间表示（IR）。酶合成梯度的任何语言编写的程序，其编译器的目标LLVM IR包括C，C++，Fortran，Julia，Rust，Swift，MLIR等，从而以这些语言提供本机AD能力。与传统的源到源和操作符重载工具不同，酶在优化的IR上执行AD。在包括Microsoft ADBench在内的机器学习重点基准测试套件中，优化IR上的AD实现了比优化前IR上的AD高4.5倍的几何平均加速，使酶实现了最先进的性能。Packaging Enzyme for PyTorch和TensorFlow提供了对具有最先进性能的外来代码梯度的方便访问，使外来代码能够直接纳入现有的机器学习工作流程。
RustMC: Extending the GenMC stateless model checker to Rust
本文提出 RustMC，通过扩展 GenMC 以支持 LLVM IR 上的并发 Rust 程序验证，解决了线程操作拦截、内存内建函数和未初始化访问等挑战，并在真实案例中有效发现不安全 Rust、FFI 调用及原子操作误用导致的并发缺陷。
Btor2MLIR: A Format and Toolchain for Hardware Verification
本文提出Btor2MLIR格式和工具链，基于MLIR框架，利用成熟编译器基础设施组件，以提升硬件验证工具的开发效率。
PrediPrune: Reducing Verification Overhead in Souper with Machine Learning Driven Pruning
本文提出 PrediPrune 随机候选剪枝策略，利用机器学习预测 Souper 优化候选有效性，减少 SMT 求解器验证负担，与 Dataflow 结合后相比 Baseline 编译时间降低 51%。
AnICA: Analyzing Inconsistencies in Microarchitectural Code Analyzers
微架构代码分析器，即，估计机器码基本块吞吐量的工具是性能工程师工具带中的重要器具。最近的工具，如llvm-mca、uiCA和Ithemal，使用各种技术和不同的模型来预测吞吐量。当进行测试时，通常会看到这些最先进的工具给出非常不同的结果。这些不一致性要么是错误，要么是工具设计者做出的不同且很少记录的假设。在本文中，我们提出了AnICA，从差分测试和抽象解释的启发，系统地分析这些代码分析器之间的不一致性的工具。我们的评估表明，AnICA可以在几十个描述中总结出数千个不一致的地方，这些描述直接导致对工具不同行为的高层次洞察。在几个案例研究中，我们进一步展示了AnICA如何自动发现和表征llvm-mca中的已知和未知错误，以及AMD Zen微架构中的一个怪癖。
Finite Countermodel Based Verification for Program Transformation (A Case Study)
自动程序验证和程序转换都是以程序分析为基础的。在过去的十年中，一些方法使用各种自动通用程序转换技术（部分演绎，专业化，超级编译）的计算系统的不可达性属性的验证被引入和演示。另一方面，基于语义的展开-折叠程序转换方法提出了各种各样的可达性任务，并试图解决它们，旨在改善被转换程序的语义树。这意味着可以使用一些通用的验证方法来加强程序转换技术。本文讨论了Turchin的超级编译方法中如何使用安全验证方法的有限反模型的问题。我们提取了一些超级编译子算法，试图解决可达性问题，并演示了使用外部countermodel查找器来解决一些问题。
QCP: A Practical Separation Logic-based C Program Verification Tool
QCP结合注解自动验证与 Rocq 交互证明，通过符号执行和分离逻辑推导求解器自动处理验证任务，同时支持 VS Code 扩展提升证明效率。
Feature-Aware Verification
软件产品线是一组软件产品，它们在功能方面有所区别（即，终端用户--可见的行为单位）。功能交互--功能组合导致紧急和可能关键的行为的情况--是软件产品线中失败的主要来源。我们探讨如何功能感知验证可以提高软件产品线中的功能交互的自动检测。产品感知验证使用产品线验证技术，并支持功能特性的规范以及单独和可组合单元中的功能。它集成了可变性编码的技术来验证产品线，而无需生成和检查可能是指数数量的特征组合。我们开发的工具套件SPLverifier功能感知验证，这是基于标准的模型检查技术。我们将其应用于包含AT&T领域知识的电子邮件系统。我们发现，功能的相互作用可以自动检测的基础上，只有功能的本地知识的规范，和变异性编码显着提高验证性能时，证明没有相互作用。
Automatic HFL(Z) Validity Checking for Program Verification
本文提出了一种自动化的方法来检验HFL（Z）公式的有效性，HFL（Z）是一种高阶逻辑，具有不动点算子和整数。结合Kobayashi et al.的减少，从高阶程序验证HFL（Z）的有效性检查，我们的方法产生一个全自动的，统一的验证方法的任意时间属性的高阶功能程序表示的模态μ演算，包括终止，非终止，公平终止，公平非终止，也分支时间属性。我们已经实现了我们的方法，并取得了可喜的实验结果。
Automatic Test Data Generation and Model Checking with CHR
我们提出了一个例子，应用约束处理规则自动测试数据生成和模型检验验证的任务关键软件的卫星控制。
Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?
本文提出NL2Contract任务，利用大型语言模型将自然语言转换为形式化功能契约（含前置与后置条件），实验证明其生成契约健全且能减少验证误报，并有效捕获真实错误。
Automatic Verification of Erlang-Style Concurrency
提出了一种自动验证Erlang式高阶并发程序安全性的方法。受Core Erlang的启发，我们引入了Lambda-Actor，这是一种具有模式匹配代数数据类型的原型函数式语言，并增加了进程创建和异步消息传递原语。我们正式的抽象模型的λ-演员程序称为演员通信系统（ACS），它有一个自然的解释为一个矢量加法系统，其中一些验证问题是可判定的。我们给出了一个参数化的抽象解释框架，并使用它来构建一个多时间可计算的，基于流的，抽象语义的Lambda-Actor程序，然后我们使用它来引导ACS的建设，从而得出一个更准确的输入程序的抽象模型。我们已经构建了Soter，一个验证方法的工具实现，从而获得了第一个全自动的，无限状态的Erlang核心片段的模型检查器。我们发现，在实践中，我们的抽象技术是准确的，足以验证一个有趣的范围内的安全属性。虽然ACS的可覆盖性问题是Expspace完备的，但Soter可以非常有效地分析这些验证问题。
Automatic verification of heap-manipulating programs
研究了命令式程序设计语言中堆组合推理的理论基础。本文提出了一种新的组合符号记忆的概念及其相关性质。我们利用这些正式的基础，建立一个组合算法，产生广义堆，符号堆演算，其特征在于任意循环代码段的条款。由这个演算推断出的所有状态都精确地对应于原始程序的可达状态。我们建立在这个演算和纯二阶函数程序的执行推理之间的对应关系。
Lightweight Interactive Proving inside an Automatic Program Verifier
在形式化方法中，演绎验证方法允许在关键软件上建立最强可能的形式化保证。缺点是设计适当的正式规范和成功履行所需的证明义务所需的人力成本。为了在工业软件开发环境中推广演绎验证，必须提供从简单和自动化方法逐步过渡到演绎验证的方法。SPARK环境，用于开发用Ada编写的关键软件，通过提供自动化工具来正式证明某些代码满足Ada合同中表达的要求，从而实现了这一目标。在利用自动证明器来履行证明义务的程序验证器中，需要一些额外的用户与证明任务的交互：或者帮助分析证明失败的原因，或者最终履行最先进的自动证明器无法达到的验证条件。在SPARK中添加交互式证明功能似乎很复杂，因为证明工具链使用了独立的中间验证工具Why 3，它足够通用，可以接受不同输入语言的多个前端。本文报告了我们的方法来扩展Why 3与交互式证明功能，并与一个通用的客户端-服务器基础设施，允许集成到一个外部的，前端的图形用户界面，如SPARK的证明交互。
Constraint-based automatic verification of abstract models of multithreaded programs
我们提出了一种多线程程序的抽象模型的自动验证技术，提供新鲜的名称生成，名称移动性和无界控制。作为高级规约语言，我们在这里采用了一个扩展的通信有限状态机的局部变量范围在一个无限的域名，称为TDL程序。通信机已被证明是非常有效的表示通信协议，以及表示多线程软件的抽象。我们提出的验证方法是基于编码的TDL程序成一个低级语言的基础上多集重写和约束，可以被看作是一个扩展的Petri网。通过这种编码，符号验证过程中开发的低级语言在我们以前的工作，现在可以应用到TDL程序。此外，编码使我们能够隔离TDL程序，仍然提供新鲜的名称生成，名称移动性和无界控制的可判定类的验证问题。我们的语法限制实际上是在线程的内部结构上定义的：为了获得一个完整的终止方法，线程最多只能有一个局部变量（范围在无限的域名上）。
Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution
在诸如分离逻辑之类的权限逻辑中，迭代分离合取是表示对堆位置的无界集合的访问权限的量词。与递归谓词相反，迭代分离合取并不规定它们所覆盖的位置的结构，因此不限制如何遍历和修改这些位置。这种灵活性对于验证随机存取数据结构（例如数组）和可以以多种方式遍历的数据结构（例如图形）是重要的。尽管它的有用性，没有自动程序验证原生支持迭代分离合取，他们是特别难以纳入符号执行引擎，流行的技术，为这些逻辑建立验证。在本文中，我们提出了第一个符号执行技术，以支持一般迭代分离合取。我们提出了一种新的表示符号堆和灵活的支持，量化堆位置的逻辑规范。我们的技术表现出可预测的和快速的性能，尽管在SMT级别采用量词，通过仔细控制量词实例。它与权限逻辑的其他功能兼容，如部分权限、递归谓词和抽象函数。我们的技术是实现作为一个扩展的毒蛇验证基础设施。
Automatic Probabilistic Program Verification through Random Variable Abstraction
最弱预期望演算已被证明是分析概率和不确定性规划定量性质的成熟理论。我们提出了一个自动的方法证明定量线性性质的任何可数状态空间使用迭代向后不动点计算的一般框架中的抽象解释。为了完成这一任务，我们提出了随机变量抽象（RVA）的技术，我们还假设了一个充分条件，实现精确的不动点计算的抽象域。我们的方法的可行性示出了两个例子，一个获得的概率程序的预期运行时间，和其他的赌博策略的预期收益。我们的方法适用于一般的保护概率和不确定性的过渡系统，而不是普通的pGCL程序，使我们能够很容易地模拟广泛的系统，包括分布式的和非结构化的程序。我们提出了该程序的操作和最弱前提语义，并证明了它的等价性。
From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
我们提出了一个有界等价性验证技术的高阶程序与局部状态。该技术结合了完全抽象的符号环境互模拟类似的符号游戏语义，新的技术，轻量级的状态不变的注释。这产生了没有假阳性或假阴性的等效性验证技术。该技术是有界完备的，因为所有的不等式都是自动检测到足够大的界限。此外，几个硬等价证明自动或后被注释与状态不变量。我们在一个名为Hobbit的工具原型中实现了该技术，并使用一组广泛的新的和现有的示例对其进行基准测试。霍比特人可以证明许多经典的等价关系，包括所有迈耶和西伯的例子。
Automatic generation and verification of test-stable floating-point code
浮点程序中的测试不稳定性发生在程序的控制流偏离其理想执行（假设为实数运算）时。这种现象是由于在条件语句中存在影响算术表达式计算的舍入错误而引起的。不稳定的测试可能会导致严重的错误，在安全关键的应用程序，依赖于数值计算。编写考虑测试不稳定性的程序是一项艰巨的任务，需要有限精度计算和舍入误差方面的专业知识。本文提出了一个工具链，自动生成和验证一个可证明正确的测试稳定的浮点程序，从一个功能规格在真正的算术。输入是用原型验证系统（PVS）规约语言编写的实值程序，输出是用ANSI/ISO C规约语言（ACSL）契约注释的转换后的浮点C程序。这些契约将浮点程序与其在实数算术中的功能规范联系起来。转换后的程序检测是否可能发生不稳定的测试，在这些情况下，发出警告并终止。提出了一种方法，它结合了框架-C分析器，PRECiSA舍入误差估计，和PVS自动验证生成的程序代码是正确的，在这个意义上说，如果程序终止没有警告，它遵循相同的计算路径作为其实值功能规范。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。