Artifact for paper (First Steps towards Deductive Verification of LLVM IR)

Artifact for paper (First Steps towards Deductive Verification of LLVM IR) submitted to FASE '24 conference. For a full description on how to use the artifact, please see the README.md file. The artifact contains a VM with the VCLLVM tool and documentation.<br>Abstract of paper<br>Over the last years, deductive program verifiers have substantially improved, and their applicability on non-trivial applicationshas been demonstrated. However, a major bottleneck is that for every new programming language, a new deductive verifier has to be built.This paper describes the first steps in a project that aims to address this problem, by developing language-agnostic support for deductive verification: Rather than building a deductive program verifier for every new programming language, we develop deductive program verification technology for a widely-used intermediate representation language (LLVM IR), such that we eventually get verification support for any new language that can be compiled into the LLVM IR format.Concretely, this paper describes the design of VCLLVM, a prototype tool that adds LLVM IR as a supported language to the VerCors verifier. We discuss the challenges that have to be addressed to develop verification support for such a low-level language. Moreover, we also sketch how we envisage to build verification support for any specified source program that can be compiled into LLVM IR on top of VCLLVM.<br>

本附属实验数据集对应提交至FASE 2024会议的论文《LLVM IR演绎验证初探》（First Steps towards Deductive Verification of LLVM IR）。有关该附属数据集的完整使用说明，请参阅README.md文件。本附属数据集包含搭载VCLLVM工具的虚拟机及配套文档。

论文摘要
近年来，演绎程序验证器已取得显著进展，其在非平凡应用场景下的适用性已得到验证。然而该领域存在一项核心瓶颈：针对每一种全新的编程语言，均需单独构建专属的演绎验证器。本文阐述了一项旨在解决该问题的项目的初步进展：我们不再为每一种新编程语言单独开发演绎程序验证器，而是针对一种广泛使用的中间表示语言（LLVM IR）开发演绎程序验证技术，最终可为所有可编译为LLVM IR格式的新编程语言提供验证支持。
具体而言，本文介绍了VCLLVM的设计方案——一款将LLVM IR作为支持语言接入VerCors验证器的原型工具。我们讨论了为这类底层语言开发验证支持时所需解决的各类挑战。此外，我们还简要勾勒了基于VCLLVM，为所有可编译至LLVM IR格式的指定源程序构建验证支持的构想。