[an error occurred while processing this directive]


Type of project:
Semesterarbeit WS 2004/2005

Daniel Kistler

Contract Prover

Supervising Assistant:
Bernd Schoeller


When developing software, quality can be of crucial importance, especially if the produced code is part of a reusable component or library. This holds not only because the quality of an application generally is only as good as its weakest part, but also because the provider hopes that the use of good components will also raise the overall quality of a software product. Therefore it is of major interest to verify that certain components act according to their specification. One approach is to examine preconditions and postconditions and to verify them step by step with the use of Hoare Logic and a theorem proving tool that guarantees the correctness of each step. But doing this completely manually can get time consuming and repetitive when verifying more than a small piece of code. Therefore it is desirable to automat and organize such work to a certain extent.