Formal verification of a constant-time preserving C compiler

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]

Possibly Related Publications

The following publications are possibly variants of this publication: