Submitted to the Dept. of Computer Science and Engineering, Seoul National University, Korea
Abstract
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.