Name | Herr Prof. Dr. Peter Müller |

Lehrgebiet | Informatik |

Adresse | Programming Methodology Group ETH Zürich, CAB H 84 Universitätstrasse 6 8092 Zürich SWITZERLAND |

Telefon | +41 44 632 28 68 |

peter.mueller@inf.ethz.ch | |

URL | http://www.pm.inf.ethz.ch |

Departement | Informatik |

Beziehung | Ordentlicher Professor |

Nummer | Titel | ECTS | Umfang | Dozierende | |
---|---|---|---|---|---|

252-0058-00L | Formal Methods and Functional Programming | 7 KP | 4V + 2U | D. Basin, P. Müller | |

Kurzbeschreibung | In this course, participants will learn about new ways of specifying, reasoning about, and developing programs and computer systems. The first half will focus on using functional programs to express and reason about computation. The second half presents methods for developing and verifying programs represented as discrete transition systems. | ||||

Lernziel | In this course, participants will learn about new ways of specifying, reasoning about, and developing programs and computer systems. Our objective is to help students raise their level of abstraction in modeling and implementing systems. | ||||

Inhalt | The first part of the course will focus on designing and reasoning about functional programs. Functional programs are mathematical expressions that are evaluated and reasoned about much like ordinary mathematical functions. As a result, these expressions are simple to analyze and compose to implement large-scale programs. We will cover the mathematical foundations of functional programming, the lambda calculus, as well as higher-order programming, typing, and proofs of correctness. The second part of the course will focus on deductive and algorithmic validation of programs modeled as transition systems. As an example of deductive verification, students will learn how to formalize the semantics of imperative programming languages and how to use a formal semantics to prove properties of languages and programs. As an example of algorithmic validation, the course will introduce model checking and apply it to programs and program designs. | ||||

252-0216-00L | Software Architecture and Engineering | 8 KP | 4V + 3U | P. Müller, M. Vechev | |

Kurzbeschreibung | This course introduces both theoretical and applied aspects of software engineering and analysis. It covers: - Software Architecture - Informal and formal Modeling - Design Patterns - Code Refactoring - Program Testing - Dynamic Program Analysis - Static Program Analysis | ||||

Lernziel | The course has two main objectives: - Obtain an end-to-end (both, theoretical and practical) understanding of the core techniques used for building quality software. - Understand how to apply these techniques in practice. | ||||

Inhalt | Some of the core technical topics covered will be: - modeling and mapping of models to code - common code design patterns - functional and structural testing - dynamic and static analysis | ||||

Literatur | Will be announced in the lecture. | ||||

264-5811-00L | Programming Systems Seminar The seminar is open to assistants of the Chair of Programming Methodology and the Software Reliability Lab (Department of Computer Science). Others should contact the instructors. | 2 KP | 2S | P. Müller, M. Vechev | |

Kurzbeschreibung | This graduate seminar provides doctoral students in computer science a chance to read and discuss current research papers. Enrollment requires permission of the instructors. Credit units are granted only to active participants. | ||||

Lernziel | Learn about current research results in the area of programming languages, static program analysis, program verification, and related areas; practice of scientific presentations. | ||||

Inhalt | The seminar will explore different topics from a research perspective. | ||||

Skript | Supporting material will be distributed during the seminar. | ||||

Voraussetzungen / Besonderes | The seminar is open to assistants of the Chair of Programming Methodology and the Software Reliability Lab (Department of Computer Science). Others should contact the instructors. |