Compilers perform two main tasks: translating source code into equivalent executable code and checking safety properties of programs (e.g., type safety), both of which are crucial for the development of reliable software. To ensure the validity of the guarantees provided by performing those tasks, two formal verification methodologies have been proposed: verified compilation for proving semantic equivalence of programs before and after compiler transformations, and verifying compilation for proving safety of programs if they pass the compilation.

Scalability in software development is achieved by dividing large programs into smaller modules with distinct responsibility, and composing the modules afterwards. For the two compiler verification methodologies above to be scalable, they must support modular verification of compiler transformations and safety checking, and composition of the verification results. We call such methods verified compositional compilation and verifying compositional compilation, respectively.

In this talk, we present our recent and ongoing work on verified and verifying compositional compilation. Firstly, a major challenge in verified compositional compilation is to support both the horizontal composition of programs written in different languages and vertical composition of multi-pass compiler correctness for open modules. We present a refinement-based verification framework to solve this problem. It allows separate verification of compiling vastly different programs (e.g., C and assembly) and composition of direct refinements between source specifications and target code, which was not possible before. The key technique is a uniform Kripke memory relation that supports both horizontal and vertical composition. Secondly, we present a framework for generically describing program safety (i.e., partial correctness in the style of separation logics) independent of any language or logic. In this framework, we investigate verifying compilation for proving absence of memory errors (e.g., use-after-free and double-free) and techniques for propagating safety from source code to all the way to executable code. This framework is being used to build a verified compiler for a subset of Rust which supports both safe and unsafe code. Finally, we discuss ongoing research on extending our framework to support concurrency.