文章基本信息

标题：Lessons Learned From Microkernel Verification — Specification is the New Bottleneck
本地全文：下载
作者：Christoph Baumann ; Bernhard Beckert ; Holger Blasum 等
期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2012
卷号：102
页码：18-32
DOI：10.4204/EPTCS.102.4
出版社：Open Publishing Association
摘要：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.