Software verification is the study of formally proving
the correctness of a program with respect to a given
specification. Even after 40 years of research and
considerable success stories in industrial applications
software verification remains an ongoing research topic.
The state of the art is that given a sufficiently rich
specification an object-oriented program can be in most
cases automatically verified using verification systems
like the KeY-System. The KeY-System is a software
verification and testing system for Java that is developed
by the research groups of Prof. Dr. Bernhard Beckert
(Univ. of Koblenz-Landau, Germany), Prof. Dr. Reiner
Hähnle (Chalmers Univ. of Tech., Sweden), and Prof. Dr.
Schmitt (University of Karlsruhe, Germany). This book
describes the theory and the implementation of the
KeY-System and the development of a prototypical version
of the KeY-System for the verification of C programs.
In particular the C dialects ANSI C, MISRA C, and C0 are
regarded.

@book{GladischDA2008,
title = {Extending {\KeY} for the Verification of C Programs},
author = {Christoph Gladisch},
publisher = {VDM Verlag},
year = {2008},
month = apr,
isbn = {978-3-639-00002-3},
url = {http://dl.acm.org/citation.cfm?id=1816864},
abstract = {Software verification is the study of formally proving
the correctness of a program with respect to a given
specification. Even after 40 years of research and
considerable success stories in industrial applications
software verification remains an ongoing research topic.
The state of the art is that given a sufficiently rich
specification an object-oriented program can be in most
cases automatically verified using verification systems
like the {\KeY}-System. The {\KeY}-System is a software
verification and testing system for Java that is developed
by the research groups of Prof. Dr. Bernhard Beckert
(Univ. of Koblenz-Landau, Germany), Prof. Dr. Reiner
H\"{a}hnle (Chalmers Univ. of Tech., Sweden), and Prof. Dr.
Schmitt (University of Karlsruhe, Germany). This book
describes the theory and the implementation of the
{\KeY}-System and the development of a prototypical version
of the {\KeY}-System for the verification of C programs.
In particular the C dialects ANSI C, MISRA C, and C0 are
regarded.}
}