Christoph Gladisch

Extending KeY for the Verification of C Programs

The Development of a Prototype

• Broschiertes Buch

Produktbeschreibung

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.

Produktdetails

• Verlag: VDM Verlag Dr. Müller / VDM Verlag Dr. Müller e.K.
• Seitenzahl: 276
• Englisch
• Abmessung: 17mm x 150mm x 220mm
• Gewicht: 427g
• ISBN-13: 9783639000023
• ISBN-10: 3639000021
• Artikelnr.: 23798445

Autorenporträt

Gladisch, Christoph§During the study of Computer Visualistics at the University of Koblenz-Landau he has first specialized in Computer Graphics and later in Artificial Intelligence, Logic, and Software Verification. In 2006 he earned his diploma and received a PhD scholarship. He is a researcher of the Artificial Intelligence Working Group in Koblenz.