Projektstart: 01.01.1997

Projektträger: Universität Augsburg

Projektverantwortung vor Ort: Prof. Dr. Bernhard Möller

Beteiligte WissenschaftlerInnen der Universität Augsburg: Dr. Thorsten Ehm, Han-Hing Dang

Zusammenfassung

Hochkomplexe Zeigerstrukturen spiele in der Informatik eine zentrale Rolle, gerade etwa in der objektorientierten Programmierung; sorgloser Umgang mit ihnen ist eine häufige Ursache schwerer Systemfehler. Daher ist die Möglichkeit einer formalen Absicherung gerade auf diesem Gebiet besonders wichtig. Es zeigt sich, dass eine spezielle Variante der Kleene-Algebra hierfür eine solide und knappe algebraische Basis liefert.
Sie erlaubt auch eine Einbeziehung der im Bereich von (gemeinsamen und verteilt benutzten) Zeigerstrukturen aktuell entwickelten Separationslogik.