Name
Abstract | ||
|---|---|---|
Wir prasentieren eine operationelle Semantik mit Typsicherheitsbeweis f¨ ur Mehr- fachvererbung in C++, formalisiert im und maschinengepruft durch den Maschinen- beweiser Isabelle/HOL. Die Typsicherheit des Vererbungsmechanismus von C++ war lange offen. Der nun vorliegende Beweis erh¨ oht das Vertrauen in die Sprache, er- zeugt aber auch neue Einsicht in die Problematik des C++-Vererbungsmechanismus. Er ¨ offnet die Tur f¨ ur weitergehende Beweise, die bisher unerreichte Sicherheitsgaran- tien f¨ ur C++-Programme liefern. |
Year | Venue | Field |
|---|---|---|
2007 | Software Engineering | Humanities,Philosophy |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
3 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Daniel Wasserrab | 1 | 61 | 5.25 |
| Tobias Nipkow | 2 | 3056 | 232.28 |
| Gregor Snelting | 3 | 982 | 94.40 |
| Frank Tip | 4 | 2197 | 132.10 |