Our moden society is built upon a plethora of complex digital systems. Hence, it is vital to ensure that this critical infrastructure is without any errors. To do so, researchers have put a lot of effort into creating programs that can prove other programs to be correct.

During his studies, Steffan Sølvsten has investigated how to improve one of the techniques that have been key to prove program correctness. In particular, he has been redesigning this technique from the ground-up such that it can scale much better for larger programs - both in theory and especially in practice. This is one more small step towards a future where we can trust our computers.

The PhD degree was completed at the Department of Computer Science, Faculty of Natural Sciences, Aarhus University.

This summary was prepared by the PhD student.

**Time**:

Thursday the 15th of May 2025 at 13.00

**Place**:

Building 5342 (Ada), room 333, Department of Computer Science, Åbogade 34, Aarhus University, 8200 Aarhus N.

**Title of Dissertation**:

I/O-efficient Symbolic Model Checking

**Contact Information**:

Steffan Christ Sølvsten, e-mail: soelvsten@cs.au.dk, tel.: +45 24772366

**Members of the Assessment Committee**:

- Professor Dirk Beyer, Department of Computer Science, Ludwig-Maximilians-Universität München, Germany

- Associate Professor Riko Jacob, Theoretical Computer Science Section, IT University of Copenhagen

- Professor Ira Assent, Department of Computer Science, Aarhus University

**Supervisor:**

- Professor Jaco van de Pol, Department of Computer Science, Aarhus University

**Language:**

The PhD dissertation will be defended in English