Durch den Aufschwung des Internets zum Kommunikationsmedium muss sich verteiltes Rechnen den Anforderungen und Betriebsbedingungen eines weitverteilten Computernetzes stellen. Ziel des Projektes ist es, das Programmierparadigma der verteilten aktiven Objekte mit dem interaktiven Theorembeweiser Isabelle/HOL zu untersuchen und Sicherheitseigenschaften zu beweisen. Der Kalkül für verteilte, asynchrone  aktive Objekte, den wir als Basis verwenden, ist ASP mit seiner Java-basierten Programmierumgebung ProActive.

Florian Kammüller • Henry Sudhof • Lilit Hakobyan • Bianca Lutz