< Retour au sommaire

Deductive Verification of LLVM-IR (and C)

Alexander Stekelenburg le

Lieu: Salle 1073

Suivre en visio

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 pointe s and structs. This talk will describe the challenges and solutions we encountered along the way.