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

Last modified: Mon Dec 8 22:30:11 2008 GMT.

Authors

Abstract

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.

Published

In Proc. Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'08), Toronto, Canada, October 2008. Lecture Notes in Computer Science Vol. 5295, pages 54-69. © 2008 Springer-Verlag.

Extended version:

Coq Implementations (354k)

colophon