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]).

 
 

Voraussetzungen	Vordiplom, Java-Kenntnisse
Arbeitsumgebung	Isabelle-Theorembeweiser
Literatur	Tobias Nipkow and David von Oheimb: Machine-checking the Java Specification: Proving Type-Saftey. Jim Alves-Foss (ed.): Formal Syntax and Semantics of Java, LNCS, Springer, Berlin, 1998 (to appear). David Syme: Proving Java Type Soundness. Jim Alves-Foss (ed.): Formal Syntax and Semantics of Java, LNCS, Springer, Berlin, 1998 (to appear). Pietro Cenciarelli and Alexander Knapp and Bernhard Reus and Martin Wirsing: An Event-Based Structural Operational Semantics of Multi-Threaded Java. Jim Alves-Foss (ed.): Formal Syntax and Semantics of Java, LNCS, Springer, Berlin, 1998 (to appear). Pietro Cenciarelli and Alexander Knapp and Bernhard Reus and Martin Wirsing: From Sequential to Multi-Threaded Java: An Event-Based Operational Semantic. Michael Johnson (ed.): Proc. 6th Int. Conf. Algebraic Methodology and Software Technology, LNCS 1349. Springer, Berlin, pp. 75--90, 1997.
Aufgabensteller	Prof. Dr. Christian Lengauer (Uni Passau), Prof. Dr. Martin Wirsing (Zweitgutachter)
Bearbeiter	Tatjana Hein, Universität Passau, email: hein@fmi.uni-passau.de
Bearbeitungszeit	Abgabe 31.03.99
Information/Betreuung	Dr. Bernhard Reus, email: reus@pst.informatik.uni-muenchen.de Tel. 2178-2178