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

Artifact for Solving Constrained Horn Clauses modulo Algebraic Data Types and Recursive Functions This page describes steps to reproduce empirical results from the paper titled “Solving Constraine...

An Uninterpreted Program (UP) is one where all variables and functions are uninterpreted. That is, all variables have the same type and functions do not have definitions. The following program is u...

We won CHC Comp again !!! Last year, we had won all tracks except LRA. This time we won ALL tracks, including LRA. Sadly, we did not improve much on LRA. This is still a big TODO. An interesting a...

We wanted to make Spacer more efficient for reasoning about Software programs (with fixed-precision numbers) and complicated hardware designs. Such problems are conveniently expressed in the first ...

Updates As I was part of organizing CHC Comp 22 and 23, Spacer could not participate officially. However, Spacer was a honours participant and won many tracks in both competitions. ...

Implemented the Buchberger algorithm for computing Grobner basis as part of a course on Symbolic computation. Links to writeup and Maple code