Researchers

 

Research

---

About Me

I am a logician by training, having done my undergraduate studies in Computer Science, Logic and Philosophy of Science at St Andrews. My research so far has been in the area of static program analysis and verification. I am also interested in the related fields of automated and interactive theorem proving, and of SAT- and SMT-solving.

Current Position

I started as a post-doc at the Microsoft Research - INRIA Joint Centre in December 2013.
I’m working on the TLA+ project. In particular, I spend my days:
- working with our project partners at CEA List on using TLA+ to verify safety properties of
communication protocols in their real time operating system PharOS;
- developing, maintaining and documenting the TLA proof manager.

Previous Positions

PhD

During my PhD studies at the University of Kent, I developed an abstract-interpretation-based backward
determinacy analysis for Prolog, and partially verified its correctness in Coq.

Internship

During an internship at MSRC I worked on SLAyer, which is a static analyser checking the memory safety of C-programs. (Try SLAyer here. :-))