cff-version: 1.2.0
abstract: "<p>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.</p><p><br></p><p>Abstract of paper</p><p><br></p><p>Over the last years, deductive program verifiers have substantially improved, and their applicability on non-trivial applications</p><p>has been demonstrated. However, a major bottleneck is that for every new programming language, a new deductive verifier has to be built.</p><p>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.</p><p>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.</p><p><br></p>"
authors:
  - family-names: Şakar
    given-names: Ömer
    orcid: "https://orcid.org/0000-0003-3457-5446"
  - family-names: van Oorschot
    given-names: Dré
  - family-names: Huisman
    given-names: Marieke
    orcid: "https://orcid.org/0000-0003-4467-072X"
title: "Artifact for paper (First Steps towards Deductive Verification of LLVM IR)"
keywords:
version: 1
identifiers:
  - type: doi
    value: 10.4121/9c8c079e-a941-4a66-89d8-3462bf30ff05.v1
license: MPL 2.0
date-released: 2024-01-11