[isabelle] Fwd: mechanical proof of Boyer-Moore fast string searching



Can anyone help J with this?


---------- Forwarded message ----------
From: J Strother Moore <moore at cs.utexas.edu>
Date: Thu, Apr 10, 2008 at 4:47 PM
Subject: mechanical proof of Boyer-Moore fast string searching
To: shankar at csl.sri.com, Mike.Gordon at cl.cam.ac.uk


Hi Shankar and Mike.  Do either of you know
whether anybody has proved the correctness of the
Boyer-Moore fast string searching algorithm in its
full form?

I know of Frank Stomp's work with PVS to prove the
preprocessing algorithm correct.  (A very nice
piece of work.)  But Stomp did not deal with the
searching itself.  Furthermore, I can't find Stomp
online any more.

Boyer and I used Nqthm to prove the correctness of
a simplified version (using "the delta1 shift") in
our 1979 book.  But the original Boyer-Moore
algorithm has a "delta2 shift" based on the
matched terminal substring, and we ignored that in
our Nqthm proof.

I recently proved the full thing correct in ACL2
as a undergrad research project and I'm wondering
if there are prior proofs.

Various Google searches did not come up with any
papers connecting the algorithm with mechanized
correctness proofs, except (references to) to the
1979 work.

If you have any clues as to who else I might ask,
please pass them on.

J






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.