Lessons Learned From Microkernel Verification — Specification is the New Bottleneck
The work
| Authors | Christoph Baumann; Bernhard Beckert; Holger Blasum; Thorsten Bormer |
|---|---|
| Editors | |
| Type | article |
| Year | 2012 |
| Citekey | baumann2012lessons |
Where it appeared
| Published in | Systems Software Verification Conference 2012 (SSV 2012) |
|---|---|
| Publisher | Open Publishing Association |
| Series | Electronic Proceedings in Theoretical Computer Science |
| Volume | 102 |
| Pages | 18--32 |
Identifiers
| arXiv | 1211.6186 from its oa_pdf_url |
|---|---|
| DOI | 10.4204/eptcs.102.4 |
| OpenAlex | W2129248173 |
Access
| Landing page | https://doi.org/10.4204/eptcs.102.4 |
|---|---|
| Free full text | https://arxiv.org/pdf/1211.6186 |
Abstract
Software verification tools have become a lot more powerful in recent years. Even verification of large, complex systems is feasible, as demonstrated in the L4.verified and Verisoft XT projects. Still, functional verification of large software systems is rare - for reasons beyond the large scale of verification effort needed due to the size alone. In this paper we report on lessons learned for verification of large software systems based on the experience gained in microkernel verification in the Verisoft XT project. We discuss a number of issues that impede widespread introduction of formal verification in the software life-cycle process.
A copy is held
pdf, 346.5 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-08-04 00:00 UTC |
| Approved by | a person 2026-08-17 14:03 UTC |
Filed under
Cite it as
@article{baumann2012lessons,
title = {Lessons Learned From Microkernel Verification — Specification is the New Bottleneck},
author = {Christoph Baumann and Bernhard Beckert and Holger Blasum and Thorsten Bormer},
year = {2012},
journal = {Systems Software Verification Conference 2012 (SSV 2012)},
publisher = {Open Publishing Association},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {102},
pages = {18--32},
doi = {10.4204/eptcs.102.4},
}
This record lives at https://refs.drheap.org/baumann2012lessons/ and will keep doing so.