Lessons Learned From Microkernel Verification – Specification is the New Bottleneck

Lessons Learned From Microkernel Verification – Specification is the New Bottleneck. Baumann, C., Beckert, B., Blasum, H., & Bormer, T. Electronic Proceedings in Theoretical Computer Science, 102:18–32, November, 2012.

Paper doi abstract bibtex

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.

@article{baumann_lessons_2012,
	title = {Lessons {Learned} {From} {Microkernel} {Verification} – {Specification} is the {New} {Bottleneck}},
	volume = {102},
	issn = {2075-2180},
	url = {http://arxiv.org/abs/1211.6186},
	doi = {10/ghv53z},
	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.},
	urldate = {2021-01-27},
	journal = {Electronic Proceedings in Theoretical Computer Science},
	author = {Baumann, Christoph and Beckert, Bernhard and Blasum, Holger and Bormer, Thorsten},
	month = nov,
	year = {2012},
	keywords = {Computer Science - Logic in Computer Science, Computer Science - Software Engineering},
	pages = {18--32},
}

Downloads: 0

{"_id":"ZtTQn9wo8cQgNHkkh","bibbaseid":"baumann-beckert-blasum-bormer-lessonslearnedfrommicrokernelverificationspecificationisthenewbottleneck-2012","author_short":["Baumann, C.","Beckert, B.","Blasum, H.","Bormer, T."],"bibdata":{"bibtype":"article","type":"article","title":"Lessons Learned From Microkernel Verification – Specification is the New Bottleneck","volume":"102","issn":"2075-2180","url":"http://arxiv.org/abs/1211.6186","doi":"10/ghv53z","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.","urldate":"2021-01-27","journal":"Electronic Proceedings in Theoretical Computer Science","author":[{"propositions":[],"lastnames":["Baumann"],"firstnames":["Christoph"],"suffixes":[]},{"propositions":[],"lastnames":["Beckert"],"firstnames":["Bernhard"],"suffixes":[]},{"propositions":[],"lastnames":["Blasum"],"firstnames":["Holger"],"suffixes":[]},{"propositions":[],"lastnames":["Bormer"],"firstnames":["Thorsten"],"suffixes":[]}],"month":"November","year":"2012","keywords":"Computer Science - Logic in Computer Science, Computer Science - Software Engineering","pages":"18–32","bibtex":"@article{baumann_lessons_2012,\n\ttitle = {Lessons {Learned} {From} {Microkernel} {Verification} – {Specification} is the {New} {Bottleneck}},\n\tvolume = {102},\n\tissn = {2075-2180},\n\turl = {http://arxiv.org/abs/1211.6186},\n\tdoi = {10/ghv53z},\n\tabstract = {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.},\n\turldate = {2021-01-27},\n\tjournal = {Electronic Proceedings in Theoretical Computer Science},\n\tauthor = {Baumann, Christoph and Beckert, Bernhard and Blasum, Holger and Bormer, Thorsten},\n\tmonth = nov,\n\tyear = {2012},\n\tkeywords = {Computer Science - Logic in Computer Science, Computer Science - Software Engineering},\n\tpages = {18--32},\n}\n\n","author_short":["Baumann, C.","Beckert, B.","Blasum, H.","Bormer, T."],"key":"baumann_lessons_2012","id":"baumann_lessons_2012","bibbaseid":"baumann-beckert-blasum-bormer-lessonslearnedfrommicrokernelverificationspecificationisthenewbottleneck-2012","role":"author","urls":{"Paper":"http://arxiv.org/abs/1211.6186"},"keyword":["Computer Science - Logic in Computer Science","Computer Science - Software Engineering"],"metadata":{"authorlinks":{}},"html":""},"bibtype":"article","biburl":"https://bibbase.org/zotero/SilverSylvester","dataSources":["YCBcQPneB9oxahSnp"],"keywords":["computer science - logic in computer science","computer science - software engineering"],"search_terms":["lessons","learned","microkernel","verification","specification","new","bottleneck","baumann","beckert","blasum","bormer"],"title":"Lessons Learned From Microkernel Verification – Specification is the New Bottleneck","year":2012}