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

Dear Yongjian,

>   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?

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

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



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