Authors
Xinyu Feng
Zhong Shao
Yu Guo
Yuan Dong
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