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.


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]

Leave a Reply

Your email address will not be published. Required fields are marked *