[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