Re: [isabelle] Formally proving the Boyer text matching algorithm
> 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