Software is everywhere!

From the apps in our phones to large-scale infrastructures that are essential for commerce, transportation, and healthcare, software enables modern life.

Ensuring that software is correct and works as intended is a challenge of societal relevance: as software infrastructures grow intertwined with many aspects of our lives, errors are costly and potentially catastrophic.

A priority for scientific and academic national bodies

Question #115 in the Nationale Wetenschapsagenda (the National Research Agenda) is “how can we build and maintain future-proof software?”.

Also, one key principle in the Digital Society Research Agenda defined by the VSNU is that systems should be trustworthy: they should be “available when needed and operate correctly and safely according to intended design”.

A longstanding scientific challenge, too

Program verification is the area of Computer Science that develops principles, methods, and tools for ensuring error-free programs. The aim is to rule out errors in programs early on, before software reaches final users.

Our research group studies how mathematics and logic can help towards this aim. Our group is also responsible for delivering education related to program verification: the courses and projects in which our BSc and MSc students learn key mathematical principles for writing correct programs.