I am honoured to be awarded the Microsoft Research PhD Fellowship.
I hope to use this funding to develop a new core for the Spacer CHC engine. I have been improving Spacer on several different domains: integers, bit-vectors, arrays, and ADTs and RFs. I want to make it easy for Spacer to reason in new domains as well e.g. non-linear arithmetic. To make this happen, I am looking to give Spacer the ability to reason about an abstraction of a theory.