| Konferenzartikel| [1] | Sabine Glesner, Program Checking with Certificates: Separating Correctness-Critical Code, Proceedings of the 12th International FME Symposium (Formal Methods Europe), p. 758-777, Springer Verlag, Lecture Notes in Computer Science, Vol. 2805, September 2003.
|
ZusammenfassungWe 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.
Autoren
| |
