This paper describes an approach to developing high
assurance system software. We demonstrate how different formal methods
can be applied in the development process by matching specific
techniques and tools to the different levels of system requirements
and how those techniques can complement each other.
System software, kernel design, theorem proving, static analysis.
@inproceedings{KleinHuuck05,
author = {Gerwin Klein and Ralf Huuck},
title = {High Assurance System Software},
booktitle = {Proc.\ 10th Australian Workshop on Safety Critical Systems and Software (SCS'05)},
year = {2005},
editor = {Tony Cant},
volume = {55},
series = {Conferences in Research and Practice in Information Technology},
address = {Sydney, Australia},
month = Aug,
publisher = {Australian Computer Society, Inc},
note = {9 pages}
}