PV1 Alive2formalises LLVM code and transformations and allows to analyse them

Collection of libraries and tools for the analysis and verification of LLVM code and transformations

Application domain/field

Type of tool

Translation validation tool for LLVM's IR

Expected input

Depends on the library/tool used.

Expected output

Depends on the library/tool used.


This framework has been made to find bugs in LLVM. Translation validation: A technique where an individual translation (e.g. a run of the compiler) is validated (i.e. verifies that the target code produced on this run correctly implements the submitted source program) instead of proving the correctness of the compiler beforehand. (Source: "Translation Validation" by A. Pnueli, M. Siegel and E. Singerman, TACAS 1998) It includes the following libraries: It includes the following tools: Uses Z3.
Compiler LLVM


Related papers

Last publication date

15 July 2021

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.