Konferenzartikel: C++ ist typsicher? Garantiert!

[wasserrab07se]

Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, Frank Tip, C++ ist typsicher? Garantiert!, Software Engineering 2007, pp. 29--31, Hamburg, Germany, March 2007.

Zusammenfassung

Wir 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.

Download

[PDF]

BibTeX

@inproceedings{wasserrab07se,
  title = {C++ ist typsicher? Garantiert!},
  booktitle = {Software Engineering 2007},
  year = {2007},
  month = mar,
  pages = {29--31},
  author = {Daniel Wasserrab and Tobias Nipkow and Gregor Snelting and Frank Tip},
  address = {Hamburg, Germany},
}

Institutsinterne Autoren

Lehrstuhlinhaber
Prof. Gregor Snelting

Ehemalige Mitarbeiter
Dr.-Ing. Daniel Wasserrab

Projekte

Projekt

CoreC++