Extending KeY for the Verification of C Programs

@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       = {https://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.}
}