Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu. Formal verification of a constant-time preserving C compiler. Proceedings of the ACM on Programming Languages, 4(POPL), 2020. [doi]
@article{BartheBGHLPT20,
title = {Formal verification of a constant-time preserving C compiler},
author = {Gilles Barthe and Sandrine Blazy and Benjamin Grégoire and Rémi Hutin and Vincent Laporte and David Pichardie and Alix Trieu},
year = {2020},
doi = {10.1145/3371075},
url = {https://doi.org/10.1145/3371075},
researchr = {https://researchr.org/publication/BartheBGHLPT20},
cites = {0},
citedby = {0},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
}