Universität München,

 Institut für Informatik,

 Lehr- und Forschungseinheit für Programmierung und Softwaretechnik 

DIPLOMARBEIT

Formalisierung einer strukturierten operationellen Semantik für multi-threaded Java in Isabelle

Zusammenfassung des vorgeschlagenen Diplomarbeitsthemas:

Die Formalisierung der operationellen Semantik von Java ist notwendig, um Korrektheit und Sicherheit (z.B. Typsicherheit) von Java-Programmen formal beweisen zu können. Eine derartige Formalisierung ist bereits für eine Teilsprache durchgeführt worden [1,2], die allerdings nur sequentielle Java-Programme umfasst.

Basierend auf der operationellen Semantik von [3,4], welche Threads beinhaltet, soll eine operationelle Semantik für multi-threaded Java in Isabelle spezifiziert werden. Aufbauend auf einer derartigen Formalisierung können nun auch semantische Eigenschaften formal mit Hilfe eines Theoremsbeweisers bewiesen werden, wie z.B. in [1] die Typsicherheit. Für den multi-threaded Fall sollen im Rahmen dieser Diplomarbeit folgende Theoreme mit Isabelle (halb)automatisch verifiziert werden:

1. Konservativität der multi-threaded Semantik mit einem Thread über eine einfachere rein sequentielle Semantik (Beweisskizze in [4]).
2. Prescient store-Events erhalten die Semantik für wohl-synchronisierte Java-Programme (Beweisskizze in [3]).