Seminar: Modelling, Analysis, and Optimization of Object-Based Systems

Summer Semester 2005
Lehrstuhl für Informatik II

Diplomstudiengang Informatik (Theoretische Informatik, Vertiefungsfach "Theorie der Programmierung")
Master Programme Software Systems Engineering (Theoretical CS, Specialisation Subject "Theory of Programming")

Contents

The goal of this seminar is to study the formal foundations of object-based systems.

Prerequisites

• Vordiplom or Bachelor in Computer Science and
• basic knowledge in object-oriented techniques, such as Java, and (preferably)
• course on Semantics of Programming Languages and/or
• course on Programmanalyse und Compileroptimierung and/or
• course on Formal Models of Concurrency and/or
• course on Model Checking.

Introduction

Topics

Thursday, 8:30am, at room 6019.

Literature

[LG00]

B. Liskov, J.V. Guttag: Program Development in Java: Abstraction, Specification, and Object-Oriented Design, Addison-Wesley, 2000

[Poe00]

A. Poetzsch-Heffter: Konzepte objektorientierter Programmierung, Springer, 2000

[BCK93]

K.B. Bruce, J. Crabtree, G. Kanapathy: An Operational Semantics for TOOPLE: A Statically-Typed Object-Oriented Programming Language, Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, LNCS 802, 1993, 603-626

[JR05]

A. Jeffrey, J. Rathke: Java Jr: Fully abstract trace semantics for a core Java language, to be published at ESOP 2005

[DE99]

S. Drossopoulou, S. Eisenbach: Describing the Semantics of Java and Proving Type Soundness, Formal Syntax and Semantics of Java, LNCS 1523, 1999, 41-82

[CKR99]

P. Cenciarelli, A. Knapp, B. Reus, M. Wirsing: An Event-Based Structural Operational Semantics of Multi-Threaded Java, Formal Syntax and Semantics of Java, LNCS 1523, 1999, 157-200

[Hen93]

A. Hense: Denotational Semantics of an Object-Oriented Programming Language with Explicit Wrappers, Formal Aspects of Computing, 5(3), 1993, 181-207

[Bru94]

K.B. Bruce: A paradigmatic object-oriented programming language: Design, static typing and semantics, Journal of Functional Programming 4(2), 1994, 127-206

[PM99]

A. Poetzsch-Heffter, P. Müller: A Programming Logic for Sequential Java, Proceedings of the 8th European Symposium on Programming Languages and Systems, LNCS 1576, 1999, 162-176

[PB03]

C. Pierik and F.S. de Boer: A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts, Formal Methods for Open Object-Based Distributed Systems, LNCS 2884, 2003, 64-78

[Kav01]

N. Kaveh: Using Model Checking to Detect Deadlocks in Distributed Object Systems, Engineering Distributed Objects: Second International Workshop, EDO 2000, LNCS 1999, 2001, 116-128

[DKR00]

D. Distefano and J.P. Katoen and A. Rensink: On a Temporal Logic for Object-Based Systems, Formal Methods for Open Object-based Distributed Systems, Kluwer Academic Publishers, 2000, 305-326

[Rum03]

B. Rumpe: Model-Based Testing of Object-Oriented Systems, Formal Methods for Components and Objects 2002, LNCS 2852, 2003, 380-402

[VHB03]

W. Visser, K. Havelund, G. Brat, S. Park, F. Lerda: Model Checking Programs, Automated Software Engineering Journal, Vol. 10, No. 2 (April 2003), 203-232

Further Resources

• How to write the manuscript (in German)
• A manuscript template (in German)
• How to give the talk (in German)
• For printed slides: seminar.sty
• For video projections: prosper.sty

Evaluation

Contact