Die CoreC++-Semantik modelliert detailgetreu die Mehrfachvererbung in C++. Die Formalisierung im Theorembeweiser Isabelle/HOL enthält neben der formalen operationalen Semantik das zugehörige C++-Typsystem und den Typsicherheitsbeweis. Dabei beschränkt sich diese Semantik auf die wesentlichen Aspekte von C++ in Bezug auf Mehrfachvererbund in Klassenhierarchien.

Ziel der Arbeit ist es, diese Semantik zusammen mit dem Typsystem und dem Typsicherheitsbeweis um Arrays zu erweitern.

• Einarbeitung in Isabelle/HOL
• Einarbeitung in die Formalisierung von CoreC++
• Erweiterung der CoreC++-Semantik und des Typsystems
• Anpassung des Typsicherheitsbeweises

Weiterhin gibt es in Isabelle/HOL einen Code-Generator, der die formalisierte Semantik ausführbar macht, der aber nicht mit der vollen Ausdrucksmächtigkeit von HOL umgehen kann. In der jetzigen Formalisierung ist die Semantik ausführbar. Wenn es möglich ist, soll auch die erweiterte Semantik wieder ausführbar sein.