Lessons Learned From Microkernel Verification
Bernhard Beckert and Thorsten Bormer
Software verification tools have become a lot more powerful in recent
years. Even verification of large, complex systems seems feasible, as
demonstrated in the L4.verified and Verisoft XT projects. Still,
functional verification of large software systems is rare. In this
paper we hint at some issues that may impede widespread introduction
of formal verification in the software lifecycle process.