Research Seminars @ Illinois

Proving Compilers Correct Using Forcing

In a world full of computers, a guarantee that a computer behaves exactly as expected is essential. The CompCert C compiler is part of a small group of computer compilers whose guarantee is mathematical proven. This correctness theorem, however, makes certain assumptions which many natural programs do not satisfy, especially in the “multithreaded” setting, where computers perform multiple task in parallel. I will present upcoming work on the foundation of mathematical logic necessary for this theorem and how to extend to the multithreaded setting. This extension uses a generalization of Scott-Solovay forcing: multithreaded programs may be forced to have a correctness theorem in the style of CompCert.