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.
Learning 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.
Performance assessment
Performance assessment information (valid until the course unit is held again)
The performance assessment is only offered in the session after the course unit. Repetition only possible after re-enrolling.
Mode of examination
written 120 minutes
Additional information on mode of examination
We offer 2 graded midterms, in the first and second half. Each midterm will be 30 minutes and act as a bonus, that is, may improve the grade, but will not make it worse. In the positive case, each midterm will count 10% of the total grade.
Written aids
None
This information can be updated until the beginning of the semester; information on the examination timetable is binding.
Performance assessment as a semester course