• [26.05.13] The next tutorial will take place on Friday the 31th at 10:15 in C003.
  
• [18.05.13] Two typos were fixed on the third exercise sheet.
• [17.05.13] The third exercise sheet was published.
  
• [13.05.13] There will be no tutorial on the 16.05.13.
  
• [03.05.13] The next tutorial will take place on Friday the 10th, at 10:15 in C003. The corresponding exercieses will be published till Monday the 6th.
  
• [02.05.13] Room and date for the lecture have changed.
• [26.04.13] Room and date for the tutorials have changed. The exercises which have to be handed-in at the beginning of the tutorial on the 2th of May are online.
  
• [24.04.13] Room and date for the lecture have changed. Further, there will be no tutorial on the 26.04.13.
  
• [17.04.13] Instead of the lecture, there will be a tutorial on the 24.04.13, at 10:15 in L109. Specifically, there will be no tutorial on the 19.04.13.
  

The course will be structured in two parts. The first part will focus on denotational and operational semantics of sequential programming languages​​, the second will introduce formalisms to specify, design, implement, analyze, and prove properties of concurrent and distributed systems. Students will learn to appreciate the semantics of programming languages ​​and to design and analyze simple concurrent systems and will acquire the skills necessary to verify the correctness of such systems through software tools. Moreover, they will acquire the necessary background for further studies and research on the theory of distributed systems.

The main topics are the following: Basic concepts of sequential and concurrent programming, discrete mathematics and proof techniques. Finite state automata and labeled transition systems. Denotational and operational semantics of programming languages​​. Domain theory and fixed points. Process Algebras and Process calculi and their models as transition systems. Behavioral equivalences as tools for abstracting from unwanted details and for minimizing systems models and as a basis for correctness proofs. Temporal and modal logics, and verification techniques of systems properties based on model checking. Quantitative (probabilistic, stochastic) variants of process calculi and their equivalences. 

 

This course will be held in English and is worth 6 ECTS.

• Fr, 9:15-11:45, Oettingenstr. 67, Room C 003
  

• Th, 16:30-18:00, Oettingenstr. 67, Room 033

• Prof. Rocco De Nicola

• Max Tschaikowski