Extending KeY for the Verification of C Programs (Paperback) (ISBN-13: 9783639000023)

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.

Author: Christoph Gladisch
ISBN-10: 3639000021
ISBN-13: 9783639000023
Publisher: VDM Verlag Dr. Mueller E.K.
Language: English
Published: 04/23/2008
Pages: 276
Format: Paperback
Weight: 0.82lbs
Size: 9.00h x 6.00w x 0.58d