[isabelle] Formally proving the Boyer text matching algorithm

Dear Isabelle experts:
   Boyer text matching algorithm  is a widely-used. See
   Do anyone have tried to prove its correctness by theorem proving.
   Or do some similar work?

   If there is no such work, can someone point the hints of using some
available theories to prove it?

Thanks in advance?


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