direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments


Program Checking with Certificates: Separating Correctness-Critical Code
Zitatschlüssel ISBN: 3-540-40828-2
Autor Sabine Glesner
Buchtitel Proceedings of the 12th International FME Symposium (Formal Methods Europe)
Seiten 758-777
Jahr 2003
Adresse Pisa, Italy
Monat Sep
Verlag Springer Verlag, Lecture Notes in Computer Science, Vol. 2805
Zusammenfassung We introduce program checking with certificates by extending the traditional notion of black-box program checking. Moreover, we establish program checking with certificates as a safety-scalable and practical method to ensure the correctness of real-scale applications. We motivate our extension of program checking with concepts of computational complexity theory and show its practical implication on the implementation and verification of checkers. Furthermore, we present an iterative method to construct checkers which is able to deal with the practically relevant problem of incomplete or missing specifications of software. In our case study, we have considered compilers and their generators, in particular code generators based on rewrite systems.
Typ der Publikation Conference Article
Download Bibtex Eintrag

Zusatzinformationen / Extras


Schnellnavigation zur Seite über Nummerneingabe