@inproceedings{bierhoff2007checking,
author = {Bierhoff, Kevin and Hawblitzel, Chris},
title = {Checking the Hardware-Software Interface in Spec#},
booktitle = {PLOS 07: 4th workshop on Programming languages and operating systems},
year = {2007},
month = {October},
abstract = {Research operating systems are often written in type-safe, high-level languages. These languages perform automatic static and dynamic checks to give basic assurances about run-time behavior. Yet such operating systems still rely on unsafe, low-level code to communicate with hardware, with little or no automated checking of the correctness of the hardware-software interaction. This paper describes experience using the Spec# language and Boogie verifier to statically specify and statically verify the safety of a driver's interaction with a network interface, including the safety of DMA.},
publisher = {Association for Computing Machinery, Inc.},
url = {http://approjects.co.za/?big=en-us/research/publication/checking-the-hardware-software-interface-in-spec/},
edition = {PLOS 07: 4th workshop on Programming languages and operating systems},
}