Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting

Explore a 21-minute conference talk from POPL 2025 that introduces Archmage and CompCertCast, the first practical framework for end-to-end verification of programs containing integer-pointer casts. Learn how researchers from Seoul National University and MPI-SWS overcome limitations in previous approaches by developing a comprehensive solution that supports important source-level coding patterns, backend optimizations, and a formal notion of out-of-memory. Discover how CompCertCast extends the CompCert verified compiler to handle integer-pointer casting with minimal overhead, and see the Archmage logic demonstrated through verification of an xor-based linked-list implementation. The presentation includes discussion of the supplementary materials, which have been evaluated as reusable artifacts. This technical talk is ideal for researchers and practitioners interested in formal verification, compiler technology, and memory models in programming languages.