The Kleene Algebra of NestedPointer Structures:Theory and ApplicationsDissertationzur Erlangung des Doktorgrades der Naturwissenschaftender Fakult¨at fur¨ Angewandte Informatikder Universit¨at Augsburgvorgelegt vonDipl.-Inf. Thorsten EhmAugsburgOktober 20031. Gutachter: Prof. Dr. Bernhard M¨oller2.hter: Prof. Dr. Rudolf BerghammerTag der mundlic¨ hen Prufung:¨ 16. Dezember 2003ZusammenfassungSoftwaregesteuerte Systeme finden mehr und mehr Eingang in unser t¨agliches Le-ben. Damit steigt auch entscheidend die Wahrscheinlichkeit, auf Grund von schlam-pig programmiertem Code mit Systemabstur¨ zen, Ausfallen¨ und fehlerhaftem Ver-halten konfrontiert zu werden. Wahr¨ end dies bei Produkten aus der Unterhaltungs-elektronik nur argerli¨ ch sein mag, kann es bei Kontrollsystemen fu¨r den Verkehr undfur¨ Kernkraftwerke oder bei medizinischen Geraten¨ lebensgef¨ahrlich sein. Anwen-dungen aus diesen Gebieten verlangen nach einem formalen Software-Entwicklungs-prozess zur Gew¨ahrleistung der Korrektheit.Obwohl es einige Methoden zur Erlangung dieses Zieles gibt, haben sich dieVerifikation und die Entwicklung korrekter Zeigeralgorithmen einer allgemeinen,formalen Behandlung weitgehend widersetzt.In dieser Arbeit werden diese Unzulanglichkeiten in zweierlei Hinsicht behandelt.¨Zuerst wird ein abstrakter Kalkul zur Behandlung von markierten Graphen und Zei-¨gerstrukturen vorgestellt.