Dmitriy Traytel: Catalogue data in Spring Semester 2019
|Name||Dr. Dmitriy Traytel|
Institut f. Informationssicherheit
ETH Zürich, CNB F 107.2
|Telephone||+41 44 632 30 23|
|252-0058-00L||Formal Methods and Functional Programming||7 credits||4V + 2U||D. Basin, P. Müller, D. Traytel|
|Abstract||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.|
|Objective||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.
|Content||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-4630-00L||Computer-Aided Modelling and Reasoning |
In the Master Programme max. 10 credits can be accounted by Labs on top of the Interfocus Courses. Additional Labs will be listed on the Addendum.
|8 credits||7P||C. Sprenger, D. Traytel|
|Abstract||The "computer-aided modelling and reasoning" lab is a hands-on course about using an interactive theorem prover to construct formal models of algorithms, protocols, and programming languages and to reason about their properties. The lab has two parts: The first introduces various modelling and proof techniques. The second part consists of a project in which the students apply these techniques|
|Objective||The students learn to effectively use a theorem prover to create unambiguous models and rigorously analyse them. They learn how to write precise and concise specifications, to exploit the theorem prover as a tool for checking and analysing such models and for taming their complexity, and to extract certified executable implementations from such specifications.|
|Content||The "computer-aided modelling and reasoning" lab is a hands-on course about using an interactive theorem prover to construct formal models of algorithms, protocols, and programming languages and to reason about their properties. The focus is on applying logical methods to concrete problems supported by a theorem prover. The course will demonstrate the challenges of formal rigor, but also the benefits of machine support in modelling, proving and validating.|
The lab will have two parts: The first part introduces basic and advanced modelling techniques (functional programs, inductive definitions, modules), the associated proof techniques (term rewriting, resolution, induction, proof automation), and compilation of the models to certified executable code. In the second part, the students work in teams of two on a project assignment in which they apply these techniques: they build a formal model and prove its desired properties. The project lies in the area of programming languages, model checking, or information security.
|Literature||Textbook: Tobias Nipkow, Gerwin Klein. Concrete Semantics, part 1 (www.concrete-semantics.org)|