Mail by Silvio Ranise 24/09/2004
---------------------------------------------------
Dear All,

Calogero told me that last GECCOO meeting was quite an exciting one
and this makes me even more sad not to have the chance to be
there... He also told me that there were questions about the actual
situation of haRVey and the possibility to use a new version.  To
answer these questions and to foster the exchange of ideas, here is a
list describing the new features we have integrated in haRVey and that
should make it more desirable:

- zChaff is now available as an alternative to BDDs

- support to discharge many proof obligations with the same back ground 
  theory

- quantifier handling: there is no more need of the external tool rvqe
to handle quantified formuale.  We have re-implemented the algorithm in C
and incorporated it in rvc: so, while you compile a proof obligation, it also
takes care of quantifiers.  The program is now very fast. We have also 
designed an alternative way to handle quantifier but its implementation 
is not yet tested and needs further preliminary tests before being included
in a release.

- arithmetic (!): we have a first version which seem to work but from time
  to time it seems to unnecessarely report satisfiability when the formula
  is unsatisfiable... This is due to a strange interplay between the 
  strategy to perform the saturation by the E prover, the decision procedure
  for arithmetic, and the protocol we have designed to make them cooperate.
  This is an issue which requires further investigations, mainly by 
  experimentation.
  So, we really need proof obligations from you all.

- theory "simplification": when considering the theory you have to model the 
various aspects of the Java language, you see that only a small fraction of 
it is used when discharging a proof obligation.  So, we devised and 
implemented a pre-processing step which heuristically squeezes the theory by 
throwing away unnecessary axioms.
  While the algorithm guarantees that if a formula is provable with the 
original theory is also provable with the squeezed theory, it is not guaranted 
that the squeezed theory is the smallest possible.  
  In this case, we were able to test the technique on two sets of proof 
obligations coming from two program verification efforts.  The results
are quite encouraging and for one of the two case studies, our system
performs much better than the one designed by the author providing the
proof obligations. Needless to say, we will be more than happy to test
this technique on the proof obligations that you will provide us.

  Also, to push further the idea on the minimization of the background
theory, we have recently designed an extended input syntax for the
system which allows to provide more structure to the theory so that
the algorithm for the simplification can perform more aggressive
simplification by exploiting such a structure.  However, don't worry
the parser is backward compatible so whatever you have in the original
syntax of the system will continue to work with the extended one.

- definition unfolding: one of the problem with superposition is that
it does not like handling formule whose main connective is a
biconditional.  This is the case for definitions, e.g. formulae of the
form \forall x.(P(x) <-> body), where body is a 1st order formula not
containing P and whose only free var is x.  So, we have implemented a
pre-processing technique which looks for such formulae in the
background theory and unfolds them in the formula to be proved.  This
technique greatly contribute to the success of the system on one of
the two case studies mentioned above for the theory minimization
technique.  For the other case study, the result is not so good:
further investigations await us in this respect and again here we are
looking forward for more proof obligations coming from you all.

After this list of feature, I hope that those interested among you (I
apologize to the others to have added yet another spam to their
mailboxes) are now motivated to use the new version of the system.
So, how can you get it?  Well, David is packing an alpha version of
the system which will be ready very soon.  The problem is that most of
the new features are not yet documented so there is a need to give a
minimal description of each one so that you can use them successfully.
As soon as it is ready, I will put it somewhere on the web so that you
can download it. 

Indeed, we are keen to receive your feedback and criticisms about
using the system but also we really need proof obligations so that we
get the feeling of which functionality is really needed.  
So far, we somehow failed to build a database of proof obligations
arising in the verification of Java programs. This is the key step to
fulfill one of the objective we have promised in the GECCOO proposal:
the characterization of new decidable theories which are important in
program verification toghether with decision procedures for them.  If
we do not know how the formulae look like, we certanly won't be able
to give syntactic characterization for them, and ultimiately we won't
be able to define the theories to which they belong.  So, in my view
and as I argued above also for the successful fulfillment of one of
the objectives of the project, it is crucial that you provide us as
much proof obligations as possible. 

Let me tell you my recent experience.  I collaborated with F. Mehta
(one of Nipkow's PhD student) on the mechanization of its proof of
Shorr-Waite algorithm.  We identified one of the key lemma and tried
haRVey on it (after translating the lemma from HOL to FOL). The system
was able to discharge the proof obligations necessary to prove the
lemma deriving from the application of the induction principle.  More
recently, with Calogero Zarba, we were able to come up with a theory
(whose decidability we are working on) in which such proof obligations
can be expressed and proved automatically by an available decision
procedure.  I think that we shall strive to obtain similar results  
from our collaborations.


I am sorry for the length of the email and I wish you a pleasant week end.

Best regards,

Silvio.