Name
Abstract | ||
|---|---|---|
This paper gives an overview of a pilot project on the specification and verification of the L4 high-performance microkernel. Of the three aspects examined in the project, we describe one in more detail: the formalisation of the kernel's Application Programming Interface using the B Method. We conclude that machine-supported formal verification of software is at a turning point; that it is now feasible, and desirable, to formally verify production-quality operating systems. |
Year | Venue | Keywords |
|---|---|---|
2006 | CATS | production-quality operating system,operating system specifica- tion,b method,machine-supported formal verification,l4 microkernel,l4 high-performance microkernel,application programming,software verification,pilot project,formal verification,operating system |
Field | DocType | ISBN |
Discrete mathematics,Functional verification,Programming language,Intelligent verification,Computer science,Microkernel,Verification,Formal methods,High-level verification,Embedded system,Software verification,Formal verification | Conference | 1-920682-33-3 |
Citations | PageRank | References |
5 | 0.55 | 9 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Rafal Kolanski | 1 | 802 | 34.23 |
| Gerwin Klein | 2 | 1450 | 87.47 |