Formally Verifying Optimizations with Block Simulations. - Léo Gourdin; Benjamin Bonneau; Sylvain Boulmé; David Monniaux; Alexandre Bérard (Proc. ACM Program. Lang., 2023)

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version). - Gaurav Parthasarathy; Thibault Dardinier; Benjamin Bonneau; Peter Müller 001; Alexander J. Summers (CoRR, 2024)

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language. - Gaurav Parthasarathy; Thibault Dardinier; Benjamin Bonneau; Peter Müller 001; Alexander J. Summers (Proc. ACM Program. Lang., 2024)