I.N. Mulder (Ike)

My research focuses on techniques for showing that programs are correct. By 'correct', we mean that a program always does what we expect (like sorting a list), and never causes critical errors (like division by zero).
In particular, I look at programs that can be executed concurrently. Think of a list that allows multiple processors to read from and write to, concurrently. This makes it a lot more complex to show correctness: we need to account for what other processes could have done to the list. Nevertheless, logics have been developed that can show correctness of these programs with a rigorous, mathematical proof.
However, these mathematical proofs are long, complicated and labor-intensive. I have developed methods to largely automate these proofs. This makes it easier to show correctness of such difficult programs.