Author of the publication

Formally Verifying Optimizations with Block Simulations.

, , , , and . Proc. ACM Program. Lang., 7 (OOPSLA2): 59-88 (October 2023)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

A Certifying Frontend for (Sub)polyhedral Abstract Domains., and . VSTTE, volume 8471 of Lecture Notes in Computer Science, page 200-215. Springer, (2014)Certifying Synchrony for Free., and . LPAR, volume 2250 of Lecture Notes in Computer Science, page 495-506. Springer, (2001)Formally verified superblock scheduling., , , , , and . CPP, page 40-54. ACM, (2022)Formally Verifying Optimizations with Block Simulations., , , , and . Proc. ACM Program. Lang., 7 (OOPSLA2): 59-88 (October 2023)The Trusted Computing Base of the CompCert Verified Compiler., and . ESOP, volume 13240 of Lecture Notes in Computer Science, page 204-233. Springer, (2022)Intuitionistic Refinement Calculus.. TLCA, volume 4583 of Lecture Notes in Computer Science, page 54-69. Springer, (2007)Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra., and . J. Autom. Reason., 62 (4): 505-530 (2019)Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles). (Programmation défensive formellement vérifiée (calculs efficaces et vérifiés en Coq, à partir d'oracles OCaml potentiellement non fiables)).. (2021)On the way to certify Computer Algebra Systems., , , , and . Calculemus, volume 23 of Electronic Notes in Theoretical Computer Science, page 370-385. Elsevier, (1999)Certified and efficient instruction scheduling: application to interlocked VLIW processors., , and . Proc. ACM Program. Lang., 4 (OOPSLA): 129:1-129:29 (2020)