Ph.D. dissertation by Youngju Song

Submitted to the Dept. of Computer Science and Engineering, Seoul National University, Korea

Thesis committee


Modern software systems are complex. To verify such a system, it is critically important to have a modular verification technique. However, none of the existing approaches are satisfactory. In this dissertation, we develop a novel modular verification technique, called RUSC (Refinement Under Self-related Contexts), and demonstrate its usefulness by applying it to both compiler verification and program verification.

On the one hand, RUSC advances the state-of-the-art on compiler verification. Specifically, we develop CompCertM, a full extension of CompCert supporting multi-language linking without any restrictions but still with low verification overhead, thus surpassing the two state-of-the-arts, CompCertX and Compositional CompCert. On the other hand, RUSC as a program verification technique is in its early stage but shows considerable potential. Compared to higher-order separation logic, our approach provides simpler specifications and stronger results, but its verification overhead is much higher and does not support advanced features yet.