Formally verified speculation and deoptimization in a JIT compiler

Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, Jan Vitek. Formally verified speculation and deoptimization in a JIT compiler. Proceedings of the ACM on Programming Languages, 5(POPL):1-26, 2021. [doi]

Abstract

Abstract is missing.