Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems

A major challenge for verifying

complete

software systems is their complexity. A complete software system consists of program modules that use many language features and span different abstraction levels (e.g. user code and run-time system code). It is extremely difficult to use one verification system (e.g. type system or Hoare-style program logic) to support all these features and abstraction levels. In our previous work, we have developed a new methodology to solve this problem. We apply specialized “domain-specific” verification systems to verify individual program modules and then link the modules in a foundational open logical framework to compose the verified complete software package. In this paper, we show how this new methodology is applied to verify a software package containing implementations of preemptive threads and a set of synchronization primitives. Our experience shows that domain-specific verification systems can greatly simplify the verification process of low-level software, and new techniques for combining domain-specific and foundational logics are critical for the successful verification of complete software systems.