Master thesis

Type of project:
Diploma thesis SS 2004

Thomas Bietenhader

Formal Semantic Specification of a Core Object-Oriented Language



In this project a formal semantic definition for a small object-oriented languag is developed, in the context of formal verification of program correctness. From its inherent modular nature, its ability to support abstraction via information hiding and subtyping, the object-oriented paradigm seems predestined for efficient reuse of software components. This raises hopes to apply these advantages also on the topic of verification. Problems arising from this enterprise are dis cussed and an overview on the actual situation of research is given. A conclusio of this discussion is that specifications become the most critical part in modul verification.

Project plan (PDF)
Final Report (PDF)