TY - DATA
T1 - Artifact for paper (First Steps towards Deductive Verification of LLVM IR)
PY - 2024/01/11
AU - Ömer Şakar
AU - Dré van Oorschot
AU - Marieke Huisman
UR - 
DO - 10.4121/9c8c079e-a941-4a66-89d8-3462bf30ff05.v1
KW - VCLLVM
KW - Deductive Verification
KW - LLVM
N2 - <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>
ER -