Séminaire LSL - Alexander Stekelenburg - Deductive Verification of LLVM-IR (and C)

Abstract

The Pallas project aims to utilize LLVM-IR as an intermediate language for deductive verification. There are a lot more programming languages than there are verifiers for these languages. By reusing the LLVM compiler framework and its intermediate representation we aim to make it as easy as possible to verify programs written in a new language. We are implementing an LLVM-IR frontend in a deductive verifier for concurrent programs called VerCors. VerCors already supports subsets of Java, C, C++, and some GPU languages like CUDA and OpenCL. In order to support LLVM-IR we needed to improve our treatment of pointers and structs. This talk will describe the challenges and solutions we encountered along the way.