Deep Specifications and Certified Abstraction Layers
Abstract
Modern computer systems consist of a multitude of abstraction layers (e.g., OS kernels, hypervisors, device drivers, network protocols), each of which defines an interface that hides the implementation details of a particular set of functionality. Client programs built on top of each layer can be understood solely based on the interface, independent of the layer implementation. Despite their obvious importance, abstraction layers have mostly been treated as a system concept; they have almost never been formally specified or verified. This makes it difficult to establish strong correctness properties, and to scale program verification across multiple layers.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 14, 2015
- Source ID
- 10.1145/2775051.2676975
Entities
People
- Haozhong Zhang
- Jérémie Koenig
- Ronghui Gu
- Shu-chun Weng
- Tahina Ramananandro
- Xiongnan (newman) Wu
- Yu Guo
- Zhong Shao
Organizations
- China Scholarship Council
- Defense Advanced Research Projects Agency
- National Natural Science Foundation of China
- National Science Foundation
- Office of Naval Research
- University of Science and Technology of China
- Yale University