Aggressive optimization without compromising end-to-end correctness guarantees.

We develop techniques and tools for integrating powerful compiler optimizations into formally verified compilation pipelines, preserving semantic correctness from source to executable code.

Our work starts with polyhedral loop transformations as a representative class of aggressive optimizations, with broader ambitions toward verified optimizing compilation.

• PolCert — Formally verified validation and code generation for polyhedral loop transformations.
• GuardCert — Verified optimistic optimization with end-to-end correctness guarantees through CompCert.