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

Doktorarbeit

Autor(en):Thorsten Bormer
Hochschule:Karlsruhe Institute of Technology
Jahr:2014
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.

BibTeX

@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.}
}