Advancing Deductive Program-Level Verification for Real-World Application: Lessons Learned from an Industrial Case Study

@phdthesis{Bormer14,
  author       = {Thorsten Bormer},
  title        = {Advancing Deductive Program-Level Verification for Real-World
                  Application: Lessons Learned from an Industrial Case Study},
  school       = {Karlsruhe Institute of Technology},
  year         = {2014},
  month        = oct,
  doi          = {10.5445/IR/1000049792},
  abstract     = {This thesis is concerned with practicability of deductive
                  program verification on source code level. As part of a case
                  study for the verification of real-world software, the
                  specification and verification approach to show correctness
                  of the virtualizing kernel PikeOS is presented. Issues within
                  the verification process using current tools and
                  methodologies are discussed and several aspects of these
                  problems are then addressed in detail to improve the
                  verification process and tool usability.}
}