direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Page Content


Program Checking with Certificates: Separating Correctness-Critical Code
Citation key ISBN: 3-540-40828-2
Author Sabine Glesner
Title of Book Proceedings of the 12th International FME Symposium (Formal Methods Europe)
Pages 758-777
Year 2003
Address Pisa, Italy
Month Sep
Publisher Springer Verlag, Lecture Notes in Computer Science, Vol. 2805
Abstract 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.
Bibtex Type of Publication Conference Article
Download Bibtex entry

Zusatzinformationen / Extras

Quick Access:

Schnellnavigation zur Seite über Nummerneingabe