Duality is a solver for Constrained Horn Clauses based on Craig Interpolation and Lazy Annotation. A CHC solver can be used for many purposes, including the verification of recursive programs.
Lazy Annotation is a method of software model checking that performs a backtracking search for a symbolic counterexample. When the search backtracks, the program is annotated with a learned fact, derived as a Craig interpolant, that constrains future search. In this sense, the method is closely analogous to conflict-driven clause learning in SAT solvers.
Getting Duality
Duality was integrated as a Horn Logic solver in the Z3 theorem prover up to version 4.7.1. Releases of Z3 containing Duality can be obtained from the Z3 Github site. To use Duality for a Horn logic problem in the SMTLIB2 format, use the Z3 command-line option engine=duality.
Paper
Lazy Annotation Revisited (Kenneth L. McMillan), In Computer Aided Verification – 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, 2014. [bibtex] [pdf] [doi]