Wasserab, DanielNipkow, TobiasSnelting, GregorTip, FrankBleek, Wolf-GideonRaasch, JörgZüllighoven, Heinz2019-05-152019-05-152007978-3-88579-199-7https://dl.gi.de/handle/20.500.12116/22771Wir präsentieren eine operationelle Semantik mit Typsicherheitsbeweis für Mehrfachvererbung in C++, formalisiert im und maschinengeprüft durch den Maschinenbeweiser Isabelle/HOL. Die Typsicherheit des Vererbungsmechanismus von C++ war lange offen. Der nun vorliegende Beweis erhöht das Vertrauen in die Sprache, erzeugt aber auch neue Einsicht in die Problematik des C++-Vererbungsmechanismus. Er öffnet die Tür für weitergehende Beweise, die bisher unerreichte Sicherheitsgarantien für C++-Programme liefern.deText/Conference Paper1617-5468