Informatisches Kolloquium WiSe 2001/2002

Dr. Thorsten Altenkich
University of Nottingham

Safe Mobile Code

Wir können Eigenschaften von Programmen logisch präzise spezifizieren, aber die Frage ob ein gegebenes Progamm eine Eigenschaft hat, ist im Allgemeinen unentscheidbar. Es ist jedoch einfach zu entscheiden, ob die Kodierung eines Beweises korrekt bezüglich eines gegebenen Herleitungskalküls ist. Auf der Basis dieser Einsicht haben Necula und Lee das Konzept von ``proof carrying code'' entwickelt, das dazu verwendet werden kann, mobilen Code mit Zertifikaten zu versehen, die automatisch geprüft werden können. Im Rahmen dieses Vortrages werde ich eine Übersicht über die Entwicklungen in diesem Bereich geben und das Potential einer ``Beweisökonomie'' diskutieren.