Memory Simulations, Security and Optimization in a Verified Compiler

Explore memory simulations, security features, and optimizations in verified compilers through this conference talk from CPP 2024. Delve into the implementation and formal verification of stack canaries, pointer authentication, and tail recursion elimination within the CompCert compiler. Gain insights into complex semantic reasoning about pointers and memory allocation, focusing on how programs maintain simulation despite altered memory layouts. Examine the intricacies of memory extensions, injections, and undefined values in the context of compiler security and optimization techniques.