@article{cs-07-1,
  title = {{Formal verification of a realistic compiler}},
  author = {Leroy, Xavier},
  journal = {Communications of the ACM},
  year = {2009},
  doi = {10.1145/1538788.1538814},
  url = {https://xavierleroy.org/publi/compcert-CACM.pdf}
}

@inproceedings{cs-07-2,
  title = {{Alive2: bounded translation validation for LLVM}},
  author = {Lopes, Nuno P. and Lee, Juneyoung and Hur, Chung-Kil and Liu, Zhengyang and Regehr, John},
  booktitle = {Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
  year = {2021},
  doi = {10.1145/3453483.3454030},
  url = {https://web.ist.utl.pt/nuno.lopes/pubs/alive2-pldi21.pdf}
}

@inproceedings{cs-07-3,
  title = {{LLVM: a compilation framework for lifelong program analysis \& transformation}},
  author = {Lattner, C. and Adve, V.},
  booktitle = {International Symposium on Code Generation and Optimization, 2004. CGO 2004.},
  year = {2004},
  doi = {10.1109/cgo.2004.1281665},
  url = {https://llvm.org/pubs/2004-01-30-CGO-LLVM.html}
}