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 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.
