Lessons Learned From Microkernel Verification — Specification is the New Bottleneck

The work

TitleLessons Learned From Microkernel Verification — Specification is the New Bottleneck
AuthorsChristoph Baumann; Bernhard Beckert; Holger Blasum; Thorsten Bormer
Typearticle
Year2012
Citekeybaumann2012lessons

Where it appeared

Published inElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
Volume102
Pages18--32

Identifiers

DOI10.4204/eptcs.102.4
OpenAlexW2129248173

Access

Landing pagehttps://doi.org/10.4204/eptcs.102.4
Free full texthttps://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.

Copy held

KindPDF, 354.8 kB
Retrieved2026-08-05
Heldlocal, for personal reference
Where it came fromhttps://arxiv.org/pdf/1211.6186

Where this came from

How it got herethe agent went looking · found via openalex
First seen2026-08-04
Standingendorsed
Approved2026-08-05
In: Electronic Proceedings in Theoretical Computer Science venue verified-memory topic

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 = {Electronic Proceedings in Theoretical Computer Science},
  volume = {102},
  pages = {18--32},
  publisher = {Open Publishing Association},
  doi = {10.4204/eptcs.102.4},
  url = {https://arxiv.org/pdf/1211.6186},
}

This record lives at https://refs.drheap.org/baumann2012lessons/ and will keep doing so.