Posts
Hari
Cancel

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 Looking forward to presenting our work at CAV 2020. (slides: ppt, pdf) We won three of the four tracks in CHC-COMP-20!!!! The paper can be found on arxiv Ex...

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

Trending Tags