What is haRVey?
haRVey is a SMT (Satisfiability Modulo Theories) prover. There are presently two branches of haRVey: haRVey-SAT and haRVey-FOL.
haRVey-FOL integrates a First-Order Logic theorem prover (hence its
name), i.e. the
E-prover. It uses the superposition calculus as implemented by the
E-prover, to determine the satisfiability of Boolean combinations of
atoms with functions interpreted in a first-order theory with
equality.
For a description of the main techniques used in haRVey-FOL, see: Alessandro Armando, Silvio Ranise and Michael Rusinowitch. A Rewriting Approach to Satisfiability Procedures. J. of Information and Computation, Volume 183, Issue 2, 15 June 2003, Pages 140-164.
haRVey-SAT is based on congruence
closure, the Nelson-Oppen framework, and rudimentary instantiation
techniques to decide the satisfiability of a set of atoms written with
uninterpreted symbols, linear arithmetics, some lambda-expressions,
and some quantifiers. The Boolean engine is a SAT solver (zChaff or MiniSAT),
hence its name.
For a description of the main techniques used in haRVey-SAT, see: Pascal Fontaine. Techniques for verification of concurrent systems with invariants. PhD Thesis, Institut Montefiore, Université de Liège, Belgium, September 2004. (PS, PS (2/sheet), bibtex)
Current developments aim at merging both branches, and provide one uniform tool. The main issues are
- the logics are different: haRVey-SAT is multi-sorted, haRVey-FOL is not
- there is some technical and theoretical difficulties to combine first-order provers within a Nelson-Oppen scheme
So, haRVey is still in development stage, but if you want to give it a try, go to the Download section.
