Seminar Formale Methoden für Java

Auf dieser Seite

• Termine
• Inhalt
• Vortragsthemen
• Einführung
• Semantik von Java
• Typsicherheit
• Semantik der Java Virtual Machine
• Verifikation

 
 

Termine

Seminar Formale Methoden für Java (2 SE)

        Zeit n.V.                          Olderog

        Vorbesprechung 
        Di, 18.7.2000, 13 Uhr c.t. 
        A3 2-214

 

Inhalt

In diesem Seminar geht um folgende Fragen:

• Was ist der formale Hintergrund von Java?
• Was bedeuten Java-Programme?
• Wie können Eigenschaften von Java-Programmen nachgewiesen werden?
• Wie wird die korrekte Ausführung von Java-Programmen sichergestellt?

Zur Beantwortung dieser Fragen sollen Originalaufsätze von 1999 und 2000 vorgetragen werden.

 

Vortragsthemen

Einführung

S. Drosspoulou, S. Eisenbach: Describing the Semantics of Java and Proving Type Soundness. In: Jim Alves-Foss, Ed., Formal Syntax and Semantics of Java, LNCS 1523, Springer-Verlag, 1999.

Semantik von Java

P. Cenciarelli, A. Knapp, B. Reus, M. Wirsing: An Event-Based Structural Operational Semantics of Multi-Threaded Java.

J. Alves-Foss, F.S. Lam: Dynamic Denotational Semantics of Java.

E. Börger, W Schulte: A Programmer Friendly Modular Definition of the semantics of Java.

All in: Jim Alves-Foss, Ed., Formal Syntax and Semantics of Java, LNCS 1523, Springer-Verlag, 1999.

Typsicherheit

D. Syme: Proving Java Type Soundness.

D. von Oheimb, T. Nipkow: Machine-Checking the Java Specification: Proving Type-Safety.

All in: Jim Alves-Foss, Ed., Formal Syntax and Semantics of Java, LNCS 1523, Springer-Verlag, 1999.

Semantik der Java Virtual Machine

Z. Qian: A Formal Specification of Java^TM Virtual Machine Instructions for Objects, Methods and Subroutines.

P.H. Hartel, M.J. Butler, M. Levy: The Operational Semantics of a Java Secure Processor.

Verifikation

J. Strother Moore: Proving Theorems about Java-Like Byte Code. In: E.-R. Olderog, B. Steffen, Eds., Correct System Design, LNCS 1710, Springer-Verlag, 1999, pp. 139-162.

M. Huisman, B. Jacobs: Java Program Verification via Hoare Logic with Abrupt Termination. In: T. Maibaum. Ed., Fundamental Approaches to Software Engineering, LNCS 1783, Springer-Verlag, 2000, pp. 284-303.