Specification and verification of object-oriented software components
Abstract:
This work presents a flexible methodology for formally specifying and deductively verifying object-oriented components.
It is based on a simple notion of program correctness. Correctness can be achieved with a novel system of proof obligations, which serve as input to a suitable theorem prover.
It is based on a simple notion of program correctness. Correctness can be achieved with a novel system of proof obligations, which serve as input to a suitable theorem prover.
| Zugehörige Institution(en) am KIT | Institut für Theoretische Informatik (ITI) |
| Publikationstyp | Hochschulschrift |
| Publikationsjahr | 2006 |
| Sprache | Deutsch |
| Identifikator | ISBN: 3-86644-042-1 urn:nbn:de:0072-45428 KITopen-ID: 1000004542 |
| Verlag | Universitätsverlag Karlsruhe |
| Umfang | XVIII, 248 S. |
| Art der Arbeit | Dissertation |
| Fakultät | Fakultät für Informatik (INFORMATIK) |
| Institut | Institut für Theoretische Informatik (ITI) |
| Prüfungsdaten | 07.02.2006 |
| Schlagwörter | formal specification, deductive verification, object-orientation, components, encapsulation, context specification, proof obligations, modular proofs |
| Referent/Betreuer | Schmitt, P. H. |