Grobner basis

We are working on a long term project of rewriting Spacer to have the theory of EUF at its core. The architecture is going to be similiar to an SMT solver: one core model checker for EUF at the cen...

We have been working on using equalities and uninterpreted functions as an abstract layer inside Spacer. A bi-product of this research was a version of model based projection centered around the th...

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 dom...