Main Page

News

Sample Solution for Problem Set 1 Problem 3

Written on 08.05.25 by Iona Kuhn

Dear students,

we just published a sample solution for Problem 3 on Problem Set 1. This is an important exercise showcasing coinduction and induction, which we discussed in the last two tutorials. Please feel free to reach out if you have further questions about it.

See you tomorrow in the tutorial!

No Lecture Next Week

Written on 25.04.25 by Arthur Correnson

Hi all!

This is a reminder that there will be no lecture next Tuesday (April 29).

We will however still offer a tutorial session next Friday (May 2nd).

Have a nice weekend!

First Problem Set and First Tutorial

Written on 23.04.25 by Arthur Correnson

Hi all!

The slides from yesterday's lecture are online, and we also released the first problem set!
We will discuss it during the first tutorial session (this Friday at 10:15 in SR 014).

See you on Friday!

First Lecture

Written on 07.04.25 (last change on 07.04.25) by Arthur Correnson

Hi all!

The semester's first lecture will take place tomorrow (08/04/2025) at 10:15 in E1.3 HS 003.
We are looking forward to meeting you there!

See you tomorrow!

PS: If you have questions about the lecture, you can write an email to arthur.correnson@cispa.de

Coinductive Proofs

The goal of this advanced lecture is to give an introduction to the notion of coinductive proofs, an elegant proof technique that finds many applications in Computer Science,
in particular in security and program verification.

Proofs by induction appear everywhere in theoretical computer science; you certainly encountered them on many occasions, starting with the lecture Programming 1.
Another essential proof method, less well-known but equally useful, is coinduction.
If you're familiar with the notion of simulation proofs (as in the lectures Concurrency and Verification), you have already dealt with a particular instance of proofs by coinduction, maybe without knowing it.

This lecture aims to present a general framework to understand the theory behind both induction and coinduction.
We will see that while induction is a suitable technique for reasoning about finite objects (e.g., data structures), coinduction gives a systematic way to reason about potentially infinite ones (e.g., program executions). This unlocks a lot of potential, in particular, to write proofs about systems and programs that may run indefinitely (e.g., web servers, microprocessors).
We will discuss applications of proofs by coinduction to security and program verification and present several advanced proof techniques that are particularly useful in this context.

Lectures will be on Tuesday 10:15 to 11:45 in E1.3 HS003
Tutorials will be on Friday 10:15 to 11:45 in E1.3 SR014