DIKU Bits: Your Code Works — But Can You Prove It Beyond Doubt?

Portrait of Ken

Speaker

Ken Friis Larsen, Associate Professor in the Programming Languages and Theory of Computation (PLTC) section

Title

Your Code Works — But Can You Prove It Beyond Doubt?

Abstract

Let's venture into the world of auto-active verification, a method that harness the power of automated theorem proving with the insight of human intellect to certify program correctness. Our exploration will be split into two main segments: first, we will tackle the verification of sorting algorithms, followed by an examination of algorithms that manipulate pointers. Through a series of live demonstrations we show how to use auto-active verification across different programming challenges.

Which courses do you teach?

I teach Proactive Computer Security (PCS) MSc, and then I'm also ofter guest lecture at other courses, for instance Software Security (SoS) MSc, and Programmering og problemløsning (PoP) BSc.

What is your favourite sketch from the DIKUrevy?

It is impossible to pick just one, but I must chose it will have to be "DIKUrevy 2014: KEN", mainly for the high quality acting. With honourable mentions to the whole topDatamat series and "DIKUrevy 2015: Ph.D.-livet"