Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
summary
Archmage defines a memory model that uses lazy valuation for int→ptr casts so the integer keeps its value until a pointer interpretation is required, allowing one‑past and other tricky cases while preserving optimizations; CompCertCast integrates Archmage into CompCert with about 24% extra source code, ~6,600 lines for cast propagation and ~3,000 lines for a physical assembly layer; cast propagation reduces register pressure and yields identical assembly when programs do not use casts; Archmage Logic (separation logic) verifies an xor linked‑list and proves soundness via an integer refines pointers theorem.
AI-written summary · about