Modular structure of the development

The Verified Software Toolchain has many components, put together in a modular way: msl . The proof theory and semantics of separation logics and indirection theory is independent of any particular programming language, independent of the memory model, independent of particular theories of concurrency. compcert . The CompCert verified C compiler is independent of any particular program logic (such as separation logic), of any particular theory of concurrency, and of the external-function context (such as an operating system-call setup). CompCert incorporates several programming languages, from C through C light to C minor and then (in various stages) to assembly languages for various target machines. The CompCert family may also include source languages such as C++ or ML. These various operational semantics all use the same memory model, and the same notion of external function call. sepcomp . The theory of separate compilation explains how to specify the compilation of a programming language that may make shared-memory external function calls, shared-memory calls to an operating system, and shared-memory interaction with other threads. This depends on CompCert's memory model, but not on any particular one of the CompCert languages. Eventually, parts of the sepcomp theory will migrate into CompCert itself. Some parts of the separate-compilation system concern modular program verifications of modular programs. We may even want to link program modules—and their verifications—written in different languages (C, ML, Java, assembly). This system requires that each language have a program logic that uses the same mpred (memory predicates) modeled using resource maps (rmap).