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]

Authors

Aurèle Barrière

This author has not been identified. Look up 'Aurèle Barrière' in Google

Sandrine Blazy

This author has not been identified. Look up 'Sandrine Blazy' in Google

Olivier Flückiger

This author has not been identified. Look up 'Olivier Flückiger' in Google

David Pichardie

This author has not been identified. Look up 'David Pichardie' in Google

Jan Vitek

This author has not been identified. It may be one of the following persons: Look up 'Jan Vitek' in Google