Re: [isabelle] Formally proving the Boyer text matching algorithm



Dear Yongjian,

>   Boyer text matching algorithm  is a widely-used. See
> http://en.wikipedia.org/wiki/Boyer%E2%80%93Moore_string_search_algorithm.
>   Do anyone have tried to prove its correctness by theorem proving.
>   Or do some similar work?

The Moore in Boyer-Moore did a proof in ACL2:

    http://www.cs.utexas.edu/~moore/publications/moore-martinez-09.pdf

This might very well be the only formal correctness proof of this algorithm.

Regards,

Jasmin





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