Theme fund: NGI Zero Core
Period: 2023-10 — 2025-01
- Seeall themes
Alive2
Translation validation for LLVM
Modern compilers, such as LLVM, perform advanced optimizations to improve performance and reduce binary size of programs. However, getting these optimizations correct is very challenging: there are many corner cases, tricky issues with undefined behavior, modular arithmetic, and so on. On the other hand, programs rely on compilers being correct. A single bug in the compiler may introduce security vulnerabilities in the compiled programs. Alive2 aims to solve this issue by verifying that LLVM is correct. It is an indispensable tool for compiler developers and for anyone that wishes to validate the compilation of their program.
- The project's own website:https://github.com/AliveToolkit/alive2/
Run by INESC-ID
This project was funded through theNGI0 Core Fund, a fund established byNLnet with financial support from the European Commission'sNext Generation Internet programme, under the aegis ofDG Communications Networks, Content and Technology under grant agreement No101092990.
