An Iris Instance for Verifying CompCert C Programs

Explore a 19-minute video presentation from the POPL 2024 conference detailing the development of an Iris instance for verifying CompCert C programs. Delve into how researchers William Mansky and Ke Du from the University of Illinois Chicago have created a program logic within the Iris framework based on CompCert, the verified C compiler. Learn about the challenges of implementing this instance, including the need for a new model of resources for CompCert memories and a novel definition of weakest preconditions and Hoare triples. Discover how this work bridges the gap between Iris and practical language semantics, enabling the verification of real C programs under the same semantics used for compilation and execution. Gain insights into the reconstruction of Verified Software Toolchain (VST) automation within this new Iris instance, and understand its potential impact on program verification for CompCert C. Access supplementary materials, including reusable artifacts, to further explore this significant contribution to program verification and interactive theorem proving.

[POPL'24] An Iris Instance for Verifying CompCert C Programs