Horn Clauses

Constrained Horn clauses have emerged recently as an intermediate layer in the process of software verification. Verification tasks from many different domains can be encoded to the common language of constrained Horn clauses (CHC) and a single CHC solver can be re-used for the actual solving. This project aims to develop an efficient and reliable CHC solver to facilitate the development and deployment of verification frameworks.

Check out our CHC solver Golem.