Peter Müller: Katalogdaten im Frühjahrssemester 2023

Name	Herr Prof. Dr. Peter Müller
Lehrgebiet	Informatik
Adresse	Professur für Software Technology ETH Zürich, CAB H 84 Universitätstrasse 6 8092 Zürich SWITZERLAND
Telefon	+41 44 632 28 68
E-Mail	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.
263-2812-00L	Program Verification	5 KP	3G + 1A	P. Müller, M. Eilers
Kurzbeschreibung	A hands-on introduction to the theory and construction of deductive program verifiers, covering both powerful techniques for formal program reasoning, and a perspective over the tool stack making up modern verification tools.
Lernziel	Students will earn the necessary skills for designing, developing, and applying deductive verification tools that enable the modular verification of complex software, including features challenging for reasoning such as heap-based mutable data and concurrency. Students will learn both a variety of fundamental reasoning principles, and how these reasoning ideas can be made practical via automatic tools. By the end of the course, students should have a good working understanding and decisions involved with designing and building practical verification tools, including the underlying theory. They will also be able to apply such tools to develop formally-verified programs.
Inhalt	The course will cover verification techniques and ways to automate them by introducing a verifier for a small core language and then progressively enriching the language with advanced features such as a mutable heap and concurrency. For each language extension, the course will explain the necessary reasoning principles, specification techniques, and tool support. In particular, it will introduce SMT solvers to prove logical formulas, intermediate verification languages to encode verification problems, and source code verifiers to handle feature-rich languages. The course will intermix technical content with hands-on experience.
Skript	The slides will be available online.
Literatur	Will be announced in the lecture.
Voraussetzungen / Besonderes	A basic familiarity with propositional and first-order logic will be assumed. Courses with an emphasis on formal reasoning about programs (such as Formal Methods and Functional Programming) are advantageous background, but are not a requirement.