Suggestion: Add front-end for Constrained Horn Clauses

ftsrg / theta

Generic, modular and configurable formal verification framework supporting various formalisms and algorithms

http://theta.inf.mit.bme.hu/

Apache License 2.0

49 stars 43 forks source link

Suggestion: Add front-end for Constrained Horn Clauses #166

Open blishko opened 2 years ago

blishko commented 2 years ago

As discussed at TACAS, it would be great if Theta could support CHC front-end. The language is a simple extension of SMT-LIB, format described here. At least transition systems (1 uninterpreted predicate and 3 clauses) and linear systems of CHCs (at most 1 uninterpreted predicate in the body of every clause) should directly map to STS and CFA in Theta's representation, I believe.

Then Theta could participate in CHC-COMP, which would be great for the CHC community.

hajduakos commented 2 years ago

Thanks @blishko for the discussion and the suggestion! I've posted this in the Theta team Slack, hopefully someone can start working on this soon.