We are experimenting with a relational logic for functional program verification. Our logic is equipped with relations over algebraic datatypes along with equality and subset-inclusion predicates over relations. Our verification procedure performs inductive program analysis (structural induction) and generates verification conditions (VCs) with sufficiently strong inductive hypotheses. VCs generated by our verification procedure adhere to the following format:
bindings <var-type bindings> in <antecedent-predicate> => <consequent-predicate> end
Here is an example VC generated by our procedure : http://pastebin.com/exncPHDA
We encode VCs thus generated in SMT2 language using following rules:
- Each concrete type (eg: 'a list) translates to an uninterpreted sort.
- Relations are encoded as uninterpreted n-ary functions from uninterpreted sorts to bool.
- Relational assertions (eg: R = R1 U R2, R = R1 X R2) are encoded as prenex-quantified assertions over uninterpreted functions.
The result of above encoding is (presumably) a formula in effectively propositional (EPR) first-order logic. With help of Z3, we were able to assert validity (unsatisfiability of negation) of many VCs. However, in some cases when VC is invalid (negation is SAT), Z3 loops. The example given above (http://pastebin.com/exncPHDA) is one such VC, whose SMT2 encoding is given here : http://pastebin.com/s8ezha7D . Z3 doesn't seem to terminate while asserting this formula.
Given that deciding quantified boolean formulas is NEXPTIME hard, non-termination of decision procedure is not very surprising. Nonetheless, we would like to know if there are any optimizations that we can do while encoding the formula in Z3 so as to make non-termination least likely -
- Our current encoding creates many empty sets (i.e., one assertion of form forall x:T, f(x)=false) and many instances of same singleton sets (i.e., forall x:T, (f(x) = true) <=> (x = v)). Does reducing such duplication help?
- Due to program elaboration, we currently have many variables and transitive equalities. Does reduction in number of variables help?
Also, how likely is it that Z3 loops while deciding an unsatisfiable quantified boolean formula?