Extending KeY for the Verification of C Programs

Book

Author(s):Christoph Gladisch
Publisher:VDM Verlag
Year:2008
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ä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.

BibTeX

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