Send in your ideas. Deadline October 1, 2024
Theme fund: NGI Zero Core
Start: 2023-10
More projects like this
Software engineering


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.


Logo NLnet: abstract logo of four people seen from above Logo NGI Zero: letterlogo shaped like a tag

This project was funded through the NGI0 Core Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 101092990.