Back to University of Twente portal
| title: | Deductive Verification for LLVM-IR |
| keywords: | program verification, llvm, deductive verification |
| topics: | Algorithms and Data Structures , Logics and semantics |
| committee: |
Description
LLVM IR is Static Single Assignment (SSA) language that aims to be an intermediate representation language.
It is light-weight and close to assembly allowing many different languages (e.g. C and SYCL) to be
compiled to LLVM and to be ran on differences devices (e.g. CPUs and GPUs), making the verification for this
language very intersting.
Verification of software aims to prove different properties (e.g. functional correctness and data-race
freedom) over the source code. There are different approaches to verifying code such as model checking
and deductive verification and there are tools supporting these approaches (see references).
Within the FMT group, we are developing a deductive verification tool VerCors for the verification
of concurrent and distributed software. It uses permission-based separation logic to reason about softwarem
specifically concurrent software.
In this project, you are asked to take a look at how LLVM code can be verified using permission-based
separation logic. Concretely, we expect you to take the following steps:
- Understand LLVM IR
- Understand separation logic, the logic VerCors uses
- Understand Viper, the intermediate verification language VerCors uses
- Identify the subset of LLVM to target
- Propose a approach to translate LLVM into Viper
- Implement the verification into the VerCors tool
References to tools that do verification on LLVM
- https://arxiv-org.ezproxy2.utwente.nl/abs/2006.02670
- https://github.com/marcelosousa/llvmvf
It is light-weight and close to assembly allowing many different languages (e.g. C and SYCL) to be
compiled to LLVM and to be ran on differences devices (e.g. CPUs and GPUs), making the verification for this
language very intersting.
Verification of software aims to prove different properties (e.g. functional correctness and data-race
freedom) over the source code. There are different approaches to verifying code such as model checking
and deductive verification and there are tools supporting these approaches (see references).
Within the FMT group, we are developing a deductive verification tool VerCors for the verification
of concurrent and distributed software. It uses permission-based separation logic to reason about softwarem
specifically concurrent software.
In this project, you are asked to take a look at how LLVM code can be verified using permission-based
separation logic. Concretely, we expect you to take the following steps:
- Understand LLVM IR
- Understand separation logic, the logic VerCors uses
- Understand Viper, the intermediate verification language VerCors uses
- Identify the subset of LLVM to target
- Propose a approach to translate LLVM into Viper
- Implement the verification into the VerCors tool
References to tools that do verification on LLVM
- https://arxiv-org.ezproxy2.utwente.nl/abs/2006.02670
- https://github.com/marcelosousa/llvmvf